LeanMachineLearning exposition

ProbabilityTheory.ProbabilityMeasure.ext_iff_coe🔗

Minimal Lean file

ext_iff_coe🔗

LemmaProbabilityTheory.ProbabilityMeasure.ext_iff_coe
Details

No docstring.

🔗theorem
ProbabilityTheory.ProbabilityMeasure.ext_iff_coe.{u_7} {α : Type u_7}
  {mα : MeasurableSpace α} {μ ν : MeasureTheory.ProbabilityMeasure α} :
  μ = ν ↔ ↑μ = ↑ν
ProbabilityTheory.ProbabilityMeasure.ext_iff_coe.{u_7}
  {α : Type u_7} {mα : MeasurableSpace α}
  {μ ν :
    MeasureTheory.ProbabilityMeasure α} :
  μ = ν ↔ ↑μ = ↑ν

Code

lemma ProbabilityMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α}
    {μ ν : ProbabilityMeasure α} :
    μ = ν ↔ (μ : Measure α) = ν

Actions: Source · Open Issue

Proof
Subtype.ext_iff