compactSpace — Mathlib

English

If X is a compact topological space and r is any equivalence relation on X, then the quotient space X/∼ is compact.

Русский

Если X — компактное топологическое пространство и ∼ — любую эквивалентность на X, то факторпространство X/∼ компактно.

LaTeX

$$$ \operatorname{CompactSpace}(X) \Rightarrow \forall r:\, X \to X \to \mathrm{Prop},\, \text{Equivalence}(r) \Rightarrow \operatorname{CompactSpace}(\operatorname{Quotient}(r)) $$$

Lean4

instance compactSpace {r : X → X → Prop} [CompactSpace X] : CompactSpace (Quot r) :=
  ⟨by
    rw [← range_quot_mk]
    exact isCompact_range continuous_quot_mk⟩

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