Theorems · Theorem · general topology

PrespectralSpace.exists_isCompact_and_isOpen_between

∀ {X : Type u_1} [inst : TopologicalSpace X] [PrespectralSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ W, IsCompact W ∧ IsOpen W ∧ K ⊆ W ∧ W ⊆ U

Defined in

Mathlib.Topology.Spectral.Prespectral

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePrespectralSpace