Theorems · Theorem · general topology

isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis

∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    (∀ (i : ι), IsLindelof (b i)) → ∀ (U : Set X), IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i

If X has a basis consisting of compact opens, then an open set in X is compact open iff it is a finite union of some elements in the basis

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