compl_mem_coLindelof

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#IsLindelof.compl_mem_coLindelof

English

If s is Lindelöf and closed, then s^c ∈ coclosedLindelof X.

Русский

Если s Линдельоф и замкнуто, то s^c принадлежит coclosedLindelof X.

LaTeX

$$$(IsLindelof\,s) \land IsClosed(s) \Rightarrow s^c \in \mathrm{coclosedLindelof}(X)$$$

Lean4

theorem _root_.IsLindelof.compl_mem_coLindelof (hs : IsLindelof s) : sᶜ ∈ coLindelof X :=
  hasBasis_coLindelof.mem_of_mem hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru