exists_isCompact_superset_iff — Mathlib

English

There exists a compact K containing s if and only if closure(s) is compact.

Русский

Существует компактное K, содержащее s, тогда и только тогда closure(s) компактно.

LaTeX

$$(∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact(closure(s))$$

Lean4

@[simp]
theorem exists_isCompact_superset_iff {s : Set X} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) :=
  ⟨fun ⟨_K, hK, hsK⟩ => hK.closure_of_subset hsK, fun h => ⟨closure s, h, subset_closure⟩⟩

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