fintypeDiv — Mathlib

English

If S ⊆ α and T ⊆ α are finite, then the quotient S / T is a finite-type set (has finitely many elements).

Русский

Если S ⊆ α и T ⊆ α конечны, то множество частного S / T конечного типа (имеет конечное число элементов).

LaTeX

$$$\\operatorname{Fin}(S) \\land \\operatorname{Fin}(T) \\Rightarrow \\operatorname{Fin}(S/T)$$$

Lean4

/-- Division preserves finiteness. -/
@[to_additive /-- Subtraction preserves finiteness. -/
    ]
instance fintypeDiv [DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] : Fintype (s / t) :=
  Set.fintypeImage2 _ _ _

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