English
If hf : s.InjOn f, then Nat.card (Set.image f s).Elem = Nat.card s.Elem.
Русский
Если hf : s.InjOn f, то Nat.card (Set.image f s).Elem = Nat.card s.Elem.
LaTeX
$$$ \forall {s} {f}, \mathrm{InjOn}\,f\,s \rightarrow \mathrm{Nat.card}(\mathrm{Set.image}\,f\,s).\mathrm{Elem} = \mathrm{Nat.card} s.\mathrm{Elem} $$$
Lean4
theorem card_image_of_injOn {f : α → β} (hf : s.InjOn f) : Nat.card (f '' s) = Nat.card s := by
classical
obtain hs | hs := s.finite_or_infinite
· have := hs.fintype
have := fintypeImage s f
simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
· have := hs.to_subtype
have := (hs.image hf).to_subtype
simp [Nat.card_eq_zero_of_infinite]