Theorems · Theorem · general topology

exists_gt_t2space

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [T2Space X]
  [LocallyCompactSpace X] (v : ShrinkingLemma.PartialRefinement u s fun w => IsCompact (closure w)),
  IsCompact s → ∀ i ∉ v.carrier, ∃ v', v < v' ∧ IsCompact (closure (v'.toFun i))

In a locally compact Hausdorff space X, if s is a compact set, v is a partial refinement, and i is an index such that i ∉ v.carrier, then there exists a partial refinement that is strictly greater than v.

Defined in

Mathlib.Topology.ShrinkingLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceLocallyCompactSpace