Theorems · Theorem · measure theory

Dense.borel_eq_generateFrom_Ioc_mem_aux

∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α},
  Dense s →
    (∀ (x : α), IsTop x → x ∈ s) →
      (∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ 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

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologySecondCountableTopology