compl_mem_coclosedCompact — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Complement of a set belongs to `coclosedCompact` if and only if its closure is compact. -/
theorem compl_mem_coclosedCompact : sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s) := by
  rw [mem_coclosedCompact_iff, compl_compl]

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