instance MeasureTheory.Option.instMeasurableSpaceOption_quasiBorelSpaces {A : Type u_1} [MeasurableSpace A] : MeasurableSpace (Option A)

Equations

• MeasureTheory.Option.instMeasurableSpaceOption_quasiBorelSpaces = MeasurableSpace.comap (Option.elim' (Sum.inl ()) Sum.inr) inferInstance

instance MeasureTheory.Option.instDiscreteMeasurableSpaceOption_quasiBorelSpaces {A : Type u_1} [MeasurableSpace A] [DiscreteMeasurableSpace A] : DiscreteMeasurableSpace (Option A)

@[simp]

theorem MeasureTheory.Option.measurable_some {A : Type u_1} [MeasurableSpace A] : Measurable some

theorem MeasureTheory.Option.measurable_elim {B : Type u_2} {C : Type u_3} [MeasurableSpace B] [MeasurableSpace C] (g : C) {h : B → C} (hh : Measurable h) : Measurable fun (x : Option B) => x.elim g h

theorem MeasureTheory.Option.measurable_elim' {B : Type u_2} {C : Type u_3} [MeasurableSpace B] [MeasurableSpace C] (g : C) {h : B → C} (hh : Measurable h) : Measurable (Option.elim' g h)

@[simp]

theorem MeasureTheory.Option.measurable_isSome {A : Type u_1} [MeasurableSpace A] : Measurable fun (x : Option A) => x.isSome

instance MeasureTheory.Option.instStandardBorelSpaceOption_quasiBorelSpaces {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] : StandardBorelSpace (Option A)