card_image_of_injective — Mathlib

English

If f is injective on s, then the image of s has the same cardinality as s.

Русский

Если f инъективна на s, то образ s имеет такую же мощность, как и само s.

LaTeX

$$$ \\forall {s : Set α} [Fintype s] {f : α → β} [Fintype (f '' s)] (H : Function.Injective f) : \\mathrm{card}(f '' s) = \\mathrm{card} s $$$

Lean4

theorem card_image_of_injective (s : Set α) [Fintype s] {f : α → β} [Fintype (f '' s)] (H : Function.Injective f) :
    Fintype.card (f '' s) = Fintype.card s :=
  card_image_of_inj_on fun _ _ _ _ h => H h

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