card_image_of_injOn — Mathlib

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]

Похожие утверждения