LeanMachineLearning exposition

1.1. ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel🔗

Properties of standard Borel spaces

Module LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel contains 1 exposed declarations.

instMeasurableEqOfStandardBorelSpace_leanMachineLearning🔗

InstanceinstMeasurableEqOfStandardBorelSpace_leanMachineLearning
Details

No docstring.

🔗theorem
instMeasurableEqOfStandardBorelSpace_leanMachineLearning.{u_1}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] :
  MeasurableEq Ω
instMeasurableEqOfStandardBorelSpace_leanMachineLearning.{u_1}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  [StandardBorelSpace Ω] : MeasurableEq Ω

Code

instance [StandardBorelSpace Ω] : MeasurableEq Ω
Used by (26)

Actions: Source · Open Issue

Proof
by
  letI := upgradeStandardBorel Ω
  infer_instance
  1. instMeasurableEqOfStandardBorelSpace_leanMachineLearning