Theorems · Theorem · general topology

isLindelof_iff_countable_subfamily_closed

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

A set s is Lindelöf if and only if for every family of closed sets whose intersection avoids s, there exists a countable subfamily whose intersection avoids s.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace