Theorems · Theorem · general topology

TopologicalSpace.secondCountableTopology_of_countable_cover

∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_1} [Countable ι] {U : ι → Set α}
  [∀ (i : ι), SecondCountableTopology ↑(U i)],
  (∀ (i : ι), IsOpen (U i)) → ⋃ i, U i = Set.univ → SecondCountableTopology α

A countable open cover induces a second-countable topology if all open covers are themselves second countable.

Defined in

Mathlib.Topology.Bases

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCountableSecondCountableTopology