compl_mem_coclosedCompact_of_isClosed

English

If s is compact and closed, then its complement is in coclosedCompact.

Русский

Если s компактно и замкнуто, то его дополнение принадлежит coclosedCompact.

LaTeX

$$$\operatorname{IsCompact}(s) \Rightarrow \operatorname{IsClosed}(s) \Rightarrow s^{c} \in \operatorname{coclosedCompact}(X)$$$

Lean4

theorem compl_mem_coclosedCompact_of_isClosed (hs : IsCompact s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedCompact X :=
  hasBasis_coclosedCompact.mem_of_mem ⟨hs', hs⟩

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