card_coeSort_mrange — Mathlib

English

If M is finite and f: M → N is an injective monoid homomorphism, then the cardinality of the image equals the cardinality of M, i.e. |Im(f)| = |M|.

Русский

Пусть M — конечный мономордовый, и f: M → N — инъективный морфизм. Тогда кардинал образа равен кардиналу M: |Im(f)| = |M|.

LaTeX

$$|Im(f)| = |M| (under injectivity of f and finiteness of M)$$

Lean4

theorem _root_.Fintype.card_coeSort_mrange {M N : Type*} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] {f : M →* N}
    (hf : Function.Injective f) : Fintype.card (mrange f) = Fintype.card M :=
  Set.card_range_of_injective hf

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