ncard_range_of_injective — Mathlib

English

If f: α → β is injective, then the cardinality of the range of f equals the cardinality of α: |range(f)| = |α|.

Русский

Если отображение f: α → β инъективно, то кардинальность образа равно кардинальности области: |range(f)| = |α|.

LaTeX

$$$$ (\text{Injective}(f)) \Rightarrow |\mathrm{range}(f)| = |\alpha| $$$$

Lean4

theorem ncard_range_of_injective (hf : Function.Injective f) : (range f).ncard = Nat.card α := by
  rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]

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