closure_subset_of_isOpen — Mathlib

English

If a compact set K is contained in an open set U, then its closure is contained in U: cl(K) ⊆ U.

Русский

Если компактное множество K вложено в открытое множество U, то его замыкание принадлежит U: \overline{K} \subseteq U.

LaTeX

$$$\overline{K} \subseteq U$$$

Lean4

/-- In an R₁ space, if a compact set `K` is contained in an open set `U`,
then its closure is also contained in `U`. -/
theorem closure_subset_of_isOpen {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) :
    closure K ⊆ U := by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

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