fintype — Mathlib

English

If α is a finite type and s is a Setoid (an equivalence relation) on α with a decidable relation, then the quotient type α modulo s is finite.

Русский

Пусть α – конечный тип, и s – множество-эквивалентность на α с разрешимостью отношения эквивалентности; тогда фактор‑тип α / s конечен.

LaTeX

$$$Fintype(\\operatorname{Quotient}(s))$$$

Lean4

instance fintype [Fintype α] (s : Setoid α) [DecidableRel ((· ≈ ·) : α → α → Prop)] : Fintype (Quotient s) :=
  Fintype.ofSurjective Quotient.mk'' Quotient.mk''_surjective

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