LeanMachineLearning exposition

ProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning🔗

Minimal Lean file

instPartialOrderFiniteMeasure_leanMachineLearning🔗

InstanceProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning
Details

No docstring.

🔗def
ProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} :
  PartialOrder (MeasureTheory.FiniteMeasure α)
ProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1}
  {mα : MeasurableSpace α} :
  PartialOrder
    (MeasureTheory.FiniteMeasure α)

Code

instance : PartialOrder (FiniteMeasure α)
Used by (3)

Actions: Source · Open Issue

Proof
PartialOrder.lift _ FiniteMeasure.toMeasure_injective