card_coeSort_range — Mathlib

English

If G is finite and f: G → N is an injective monoid homomorphism, then the cardinality of the range of f equals the cardinality of G.

Русский

Если G конечна и f: G → N — инъективный гомоморфизм моноидов, то кардинал образа f равен кардиналу G.

LaTeX

$$|Im(f)| = |G|$$

Lean4

theorem _root_.Fintype.card_coeSort_range [Fintype G] [DecidableEq N] {f : G →* N} (hf : Function.Injective f) :
    Fintype.card (range f) = Fintype.card G :=
  Set.card_range_of_injective hf

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