Theorems · Theorem · general topology

IsCompact.elim_nhds_subcover_nhdsSet

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {U : X → Set X}, (∀ x ∈ s, U x ∈ nhds x) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ nhdsSet s

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace