Documentation

Verification.ProbabilityUnitBorel

← Mathematical handbook
source
instance Verification.probabilityUnitOpensMeasurable :
OpensMeasurableSpace (MeasureTheory.ProbabilityMeasure ↑unitInterval)
source
instance Verification.probabilityUnitBorel :
BorelSpace (MeasureTheory.ProbabilityMeasure ↑unitInterval)

On laws on the unit interval, the Giry and weak Borel structures agree.

source
instance Verification.probabilityUnitPolish :
PolishSpace (MeasureTheory.ProbabilityMeasure ↑unitInterval)