LeanMachineLearning exposition

ProbabilityTheory.FiniteMeasure.le_iff_coe🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

le_iff_coe🔗

LemmaProbabilityTheory.FiniteMeasure.le_iff_coe
Details

No docstring.

🔗theorem
ProbabilityTheory.FiniteMeasure.le_iff_coe.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {μ ν : MeasureTheory.FiniteMeasure α} :
  μ ≤ ν ↔ ↑μ ≤ ↑ν
ProbabilityTheory.FiniteMeasure.le_iff_coe.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ ν : MeasureTheory.FiniteMeasure α} :
  μ ≤ ν ↔ ↑μ ≤ ↑ν

Code

lemma FiniteMeasure.le_iff_coe {μ ν : FiniteMeasure α} :
    μ ≤ ν ↔ (μ : Measure α) ≤ (ν : Measure α)
Type uses (1)
Used by (2)

Actions: Source · Open Issue

Proof
Iff.rfl

Dependency graph

Type dependencies (1)

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