instLindelofSpaceSum — Mathlib

English

The disjoint union of two Lindelöf spaces is Lindelöf.

Русский

Дисъюнкция двух Линдельфовых пространств Линдельфово.

LaTeX

$$$\\text{LindelofSpace}(X) \\to \\text{LindelofSpace}(Y) \\Rightarrow \\text{LindelofSpace}(X \\oplus Y).$$$

Lean4

/-- The disjoint union of two Lindelöf spaces is Lindelöf. -/
instance [LindelofSpace X] [LindelofSpace Y] : LindelofSpace (X ⊕ Y) where
  isLindelof_univ := by
    rw [← range_inl_union_range_inr]
    exact (isLindelof_range continuous_inl).union (isLindelof_range continuous_inr)

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