LeanMachineLearning exposition

instMeasurableEqOfStandardBorelSpace_leanMachineLearning🔗

Minimal Lean file

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