HereditarilyLindelof_LindelofSets

English

For any HereditarilyLindelofSpace X and any subset s ⊆ X, s is Lindelöf.

Русский

Для пространства X с свойством наследуемой линдельфовости и любого подмножества s ⊆ X, s — Линдельфово.

LaTeX

$$$[HereditarilyLindelofSpace X] (s: Set X), IsLindelof s.$$$

Lean4

theorem HereditarilyLindelof_LindelofSets [HereditarilyLindelofSpace X] (s : Set X) : IsLindelof s :=
  by
  apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ
  exact subset_univ s

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