LeanMachineLearning exposition

ProbabilityTheory.FiniteMeasure.ext_iff_coe🔗

Minimal Lean file

ext_iff_coe🔗

LemmaProbabilityTheory.FiniteMeasure.ext_iff_coe
Details

No docstring.

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

Code

lemma FiniteMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α} {μ ν : FiniteMeasure α} :
    μ = ν ↔ (μ : Measure α) = ν
Used by (1)

Actions: Source · Open Issue

Proof
Subtype.ext_iff