Theorems · Theorem · general topology

IsLindelof.elim_nhds_subcover

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

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace