Theorems · Theorem · general topology

exists_countable_generateFrom_Ioi_Iio

∀ (α : Type u) [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] [SecondCountableTopology α],
  ∃ c, c.Countable ∧ ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}

In a second countable topological space with the order topology, the topology is generated by half-infinite open intervals with endpoints in a countable set.

Defined in

Mathlib.Topology.Order.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderOrderTopologySecondCountableTopology