Documentation

Linglib.Core.MeasureTheory.MeasurableSpace.Sum

Singletons in a sum of measurable spaces #

A singleton in α ⊕ β is the image of a singleton under Sum.inl or Sum.inr, so it is measurable when singletons in α and β are. [UPSTREAM] candidate for Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean.

instance Sum.instMeasurableSingletonClass {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] :
MeasurableSingletonClass (α ⊕ β)