Theorems · Theorem · measure theory

Dense.borel_eq_generateFrom_Ioc_mem

∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [DenselyOrdered α] [NoMaxOrder α] {s : Set α},
  Dense s → borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologySecondCountableTopologyDenselyOrderedNoMaxOrder