card_range_of_injective — Mathlib

English

If f is injective and α is finite, then the cardinality of the range of f equals the cardinality of α.

Русский

Если f инъективна и α конечно, то мощность образа f равна мощности α.

LaTeX

$$$ [Fintype α] \\; {f : α \\to β} \\; (hf : Injective f) \\; [Fintype (range f)] : \\mathrm{card}(range f) = \\mathrm{card}(α) $$$

Lean4

theorem card_range_of_injective [Fintype α] {f : α → β} (hf : Injective f) [Fintype (range f)] :
    Fintype.card (range f) = Fintype.card α :=
  Eq.symm <| Fintype.card_congr <| Equiv.ofInjective f hf

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