compl_mem_coclosedLindelof_of_isClosed

English

If s is Lindelöf and closed, then its complement lies in coclosedLindelof.

Русский

Если s Линдельоф и замкнуто, то его дополнение лежит в coclosedLindelof.

LaTeX

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

Lean4

theorem compl_mem_coclosedLindelof_of_isClosed (hs : IsLindelof s) (hs' : IsClosed s) :
    sᶜ ∈ Filter.coclosedLindelof X :=
  hasBasis_coclosedLindelof.mem_of_mem ⟨hs', hs⟩

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