card_range — Mathlib

English

If f: α → β is an embedding between finite types, then card(range f) = card α.

Русский

Если f: α → β — вложение между конечными типами, тогда card(range f) = card α.

LaTeX

$$$f:\alpha \to \beta$ embedding \Rightarrow |\operatorname{range}(f)| = |\alpha|$$

Lean4

theorem card_range {α β F : Type*} [FunLike F α β] [EmbeddingLike F α β] (f : F) [Fintype α] [Fintype (Set.range f)] :
    Fintype.card (Set.range f) = Fintype.card α :=
  Eq.symm <| Fintype.card_congr <| Equiv.ofInjective _ <| EmbeddingLike.injective f

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