card_quotient_le — Mathlib

English

For a finite α and any Setoid s on α, the cardinality of the quotient α/≈ is at most the cardinality of α.

Русский

Для конечного α и любого множества-эквивалентности s на α кардинальность фактор-меры α/≈ не превосходит кардинальность α.

LaTeX

$$$|\mathrm{Quotient}(s)| \le |\alpha|$$$

Lean4

theorem card_quotient_le [Fintype α] (s : Setoid α) [DecidableRel ((· ≈ ·) : α → α → Prop)] :
    Fintype.card (Quotient s) ≤ Fintype.card α :=
  Fintype.card_le_of_surjective _ Quotient.mk'_surjective

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