The measurable space on Option

Option α carries the image of the σ-algebra of α under some: a set is measurable when its preimage under some is. The point none is an atom, some is a measurable embedding, and the space is discrete when α is.

Main results

• measurableEmbedding_some: some is a measurable embedding.
• Option.measurableSet_iff: measurability is measurability of the preimage under some.

@[instance_reducible]

instance Option.instMeasurableSpace {α : Type u_1} [m : MeasurableSpace α] : MeasurableSpace (Option α)

Equations

• Option.instMeasurableSpace = MeasurableSpace.map some m

theorem Option.measurableSet_iff {α : Type u_1} [m : MeasurableSpace α] {s : Set (Option α)} : MeasurableSet s ↔ MeasurableSet (some ⁻¹' s)

theorem Option.measurableSet_singleton_none {α : Type u_1} [m : MeasurableSpace α] : MeasurableSet {none}

theorem Option.measurable_some {α : Type u_1} [m : MeasurableSpace α] : Measurable some

instance Option.instMeasurableSingletonClass_linglib {α : Type u_1} [m : MeasurableSpace α] [MeasurableSingletonClass α] : MeasurableSingletonClass (Option α)

instance Option.instDiscreteMeasurableSpace_linglib {α : Type u_1} [m : MeasurableSpace α] [DiscreteMeasurableSpace α] : DiscreteMeasurableSpace (Option α)

theorem measurableEmbedding_some {α : Type u_1} [MeasurableSpace α] : MeasurableEmbedding some