Theorems · Theorem · general topology

isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom

∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] (c : Set α),
  ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a} →
    TopologicalSpace.IsTopologicalBasis
      {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Set.Ioi a) ∩ ⋂ a ∈ g, Set.Iio a}

If a topology is generated by half-open intervals with endpoints in a set c, then the sets formed by intersecting finitely many of these intervals form a topological basis.

Defined in

Mathlib.Topology.Order.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorder