instFiniteQuotientOfCompactSpace — Mathlib

English

If X is compact, then every discrete quotient S of X is finite; equivalently, the quotient space S.toSetoid is a finite set.

Русский

Если X компактно, то каждый дискретный фактор пространства X конечен; эквивалентно тому, что фактор-пространство S.toSetoid является конечным множеством.

LaTeX

$$$\\text{Finite}(\\operatorname{Quotient}(S.toSetoid))$$$

Lean4

/-- If `X` is a compact space, then any discrete quotient of `X` is finite. -/
instance [CompactSpace X] : Finite S :=
  by
  have : CompactSpace S := Quotient.compactSpace
  rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this

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