theorem Combinatorics.Injective.cardinality_inj' {m n : Nat} {β : Type u} [Finite β] (h2 : (Finite.ftype β).cardinality = n) {α : Type u} [Finite α] : (Finite.ftype α).cardinality = m → m ≤ n → (n - m).factorial * (Finite.ftype (Function.Injection α β)).cardinality = n.factorial

theorem Combinatorics.Injective.cardinality_inj {α β : Type u} [Finite α] [Finite β] (h : (Finite.ftype α).cardinality ≤ (Finite.ftype β).cardinality) : ((Finite.ftype β).cardinality - (Finite.ftype α).cardinality).factorial * (Finite.ftype (Function.Injection α β)).cardinality = (Finite.ftype β).cardinality.factorial

theorem Combinatorics.Injective.cardinality_inj_div {α β : Type u} [Finite α] [Finite β] (h : (Finite.ftype α).cardinality ≤ (Finite.ftype β).cardinality) : (Finite.ftype (Function.Injection α β)).cardinality = (Finite.ftype β).cardinality.factorial / ((Finite.ftype β).cardinality - (Finite.ftype α).cardinality).factorial

theorem Combinatorics.Injective.cardinality_inj_self {α : Type u} [Finite α] : (Finite.ftype (Function.Injection α α)).cardinality = (Finite.ftype α).cardinality.factorial

theorem Combinatorics.Bijective.cardinality_bij_self {α : Type u} [Finite α] : (Finite.ftype (Function.Bijection α α)).cardinality = (Finite.ftype α).cardinality.factorial

theorem Combinatorics.Surjective.cardinality_surj_self {α : Type u} [Finite α] : (Finite.ftype (Function.Surjection α α)).cardinality = (Finite.ftype α).cardinality.factorial

theorem Combinatorics.Bijective.cardinality_bij {α β : Type u} [Finite α] [Finite β] (h : Equipotent α β) : (Finite.ftype (Function.Bijection α β)).cardinality = (Finite.ftype α).cardinality.factorial