Theorems · Theorem · general topology

TopologicalSpace.isOpen_iUnion_countable

∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (s : ι → Set α),
  (∀ (i : ι), IsOpen (s i)) → ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

In a second-countable space, an open set, given as a union of open sets, is equal to the union of countably many of those sets. In particular, any open covering of α has a countable subcover: α is a Lindelöf space.

Defined in

Mathlib.Topology.Bases

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSecondCountableTopology