f : StieltjesFunction
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ OuterMeasure.caratheodory (StieltjesFunction.outer f)
f : StieltjesFunction
⊢ borel ℝ ≤ OuterMeasure.caratheodory (StieltjesFunction.outer f)
rw [borel_eq_generateFrom_Ioi]
f : StieltjesFunction
⊢ ∀ (t : Set ℝ), t ∈ range Ioi → MeasurableSet t
f : StieltjesFunction
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ OuterMeasure.caratheodory (StieltjesFunction.outer f)
refine' MeasurableSpace.generateFrom_le _
no goals
f : StieltjesFunction
⊢ ∀ (t : Set ℝ), t ∈ range Ioi → MeasurableSet t
simp (config := { contextual := true }) [f.measurableSet_Ioi]