English
For finite α and β, the number of embeddings α ↪ β equals the falling factorial (|β|)_{|α|}, i.e., the number of injective maps from α to β.
Русский
Для конечных α и β число вложений α ↪ β равно падению факториала (|β|)_{|α|}, то есть числу инъективных отображений α в β.
LaTeX
$$$$ \lvert \alpha \hookrightarrow \beta \rvert = (\lvert \beta \rvert)_{\!\lvert \alpha \rvert} $$$$
Lean4
@[simp]
theorem card_embedding_eq {α β : Type*} [Fintype α] [Fintype β] [emb : Fintype (α ↪ β)] :
‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖ :=
by
rw [Subsingleton.elim emb Embedding.fintype]
refine
Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) (fun α₁ α₂ h₂ e ih ↦ ?_) (?_)
(fun γ h ih ↦ ?_) α <;>
dsimp only at * <;>
clear! α
· letI := Fintype.ofEquiv _ e.symm
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
· rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
exact ⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩
·
classical
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β), card_sigma, ← ih]
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ, Nat.nsmul_eq_mul,
mul_comm]
