Documentation

LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel

Properties of standard Borel spaces #

source
instance instMeasurableEqOfStandardBorelSpace_leanMachineLearning {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] :
MeasurableEq Ω