compactSpace — Mathlib

English

Let X be a compact space and r a Setoid on X; the quotient space X/ r is compact.

Русский

Пусть X — компактное пространство, и r — эквивалентность на X; факторпространство X / r компактно.

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 {s : Setoid X} [CompactSpace X] : CompactSpace (Quotient s) :=
  Quot.compactSpace

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