nonLindelof_univ — Mathlib

English

For any X that is NonLindelofSpace, the universal set (the whole space) is not Lindelöf.

Русский

Для пространства X, не являющегося Линдельфовым, сам универсум не является Линдельфовым.

LaTeX

$$$(X: Type*)\ [TopologicalSpace X] [NonLindelofSpace X] : ¬IsLindelof (univ : Set X)$$$

Lean4

theorem nonLindelof_univ (X : Type*) [TopologicalSpace X] [NonLindelofSpace X] : ¬IsLindelof (univ : Set X) :=
  NonLindelofSpace.nonLindelof_univ

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