Theorems · Theorem · general topology

IsCompact.closure_subset_of_isOpen

∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K : Set X},
  IsCompact K → ∀ {U : Set X}, IsOpen U → K ⊆ U → closure K ⊆ U

In an R₁ space, if a compact set K is contained in an open set U, then its closure is also contained in U.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

9 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceR1Space