ne_univ — Mathlib

English

If X is a non-Lindelöf space, then no Lindelöf subset can be the whole space; i.e., s is not equal to univ whenever s is Lindelöf.

Русский

Если пространство X не Линделёфово, то ни одно подмножество, обладающее свойством Линделёфа, не может быть всего пространством; то есть s ≠ univ.

LaTeX

$$$ [NonLindelofSpace X] (IsLindelof s) \\rightarrow s \\neq univ $$$

Lean4

theorem ne_univ [NonLindelofSpace X] (hs : IsLindelof s) : s ≠ univ := fun h ↦ nonLindelof_univ X (h ▸ hs)

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