Theorems · Theorem · general topology

IsLindelof.elim_countable_subfamily_closed

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsLindelof s →
    ∀ (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

For every family of closed sets whose intersection avoids a Lindelöf set, there exists a countable subfamily whose intersection avoids this Lindelöf set.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace