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 (α ⊕ β)