Theorems · Theorem · general topology

SeparatedNhds.of_isCompact_isCompact_isClosed

∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K L : Set X},
  IsCompact K → IsCompact L → IsClosed L → Disjoint K L → SeparatedNhds K L

If K and L are disjoint compact sets in an R₁ topological space and L is also closed, then K and L have disjoint neighborhoods.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1Space