LeanPool.QuasiBorelSpaces.MeasureTheory.Sum #
Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.Sum.
instance
Sum.instBorelSpace_leanPool
{A : Type u_1}
{B : Type u_2}
[MeasurableSpace A]
[MeasurableSpace B]
[TopologicalSpace A]
[hA : BorelSpace A]
[TopologicalSpace B]
[hB : BorelSpace B]
:
BorelSpace (A ⊕ B)
instance
Sum.instStandardBorelSpace_leanPool
{A : Type u_1}
{B : Type u_2}
[MeasurableSpace A]
[MeasurableSpace B]
[StandardBorelSpace A]
[StandardBorelSpace B]
:
StandardBorelSpace (A ⊕ B)
instance
Sum.instDiscreteMeasurableSpace_leanPool
{A : Type u_1}
{B : Type u_2}
[MeasurableSpace A]
[MeasurableSpace B]
[DiscreteMeasurableSpace A]
[DiscreteMeasurableSpace B]
:
DiscreteMeasurableSpace (A ⊕ B)