card_image_of_injective — Mathlib

English

Let f: A → B be injective and S ⊆ A. Then the cardinality of the image f[S] equals the cardinality of S.

Русский

Пусть f: A → B инъективно отображает A в B, и S ⊆ A. Тогда кардинальность образа f[S] равна кардинальности S.

LaTeX

$$$$ \forall S \subseteq A, \; |f[S]| = |S| $$$$

Lean4

theorem card_image_of_injective {f : α → β} (hf : Injective f) (s : Set α) : Nat.card (f '' s) = Nat.card s :=
  card_image_of_injOn hf.injOn

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