LindelofSpace — Mathlib

English

If X is Lindelöf, then the quotient space X/~ is Lindelöf for any equivalence relation ~ on X.

Русский

Если X Линдельфово, то факторпространство X/~ Линдельфово при любой эквивалентности на X.

LaTeX

$$$[\\text{LindelofSpace } X] \\Rightarrow \\operatorname{LindelofSpace}(\\operatorname{Quotient}~).$$$

Lean4

instance LindelofSpace {r : X → X → Prop} [LindelofSpace X] : LindelofSpace (Quot r) where
  isLindelof_univ := by
    rw [← range_quot_mk]
    exact isLindelof_range continuous_quot_mk

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