English
If f is injective on s, then the cardinality of f(s) equals the cardinality of s.
Русский
Если f инъективна на s, то мощность образа f(s) равна мощности s.
LaTeX
$$$ \\forall s : Set α, \\text{[Fintype s]} \\; [Fintype (f '' s)] \\; (H) : \\; \\mathrm{card}(f''s) = \\mathrm{card}(s) $$$
Lean4
theorem card_image_of_inj_on {s : Set α} [Fintype s] {f : α → β} [Fintype (f '' s)]
(H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) : Fintype.card (f '' s) = Fintype.card s :=
haveI := Classical.propDecidable
calc
Fintype.card (f '' s) = (s.toFinset.image f).card := Fintype.card_of_finset' _ (by simp)
_ = s.toFinset.card :=
(Finset.card_image_of_injOn fun x hx y hy hxy => H x (mem_toFinset.1 hx) y (mem_toFinset.1 hy) hxy)
_ = Fintype.card s := (Fintype.card_of_finset' _ fun _ => mem_toFinset).symm
