LeanMachineLearning exposition

ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl🔗

Minimal Lean file

coe_refl🔗

LemmaProbabilityTheory.Kernel.MeasurableEquiv.coe_refl
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl.{u_3} {α : Type u_3}
  {mα : MeasurableSpace α} : ⇑(MeasurableEquiv.refl α) = id
ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl.{u_3}
  {α : Type u_3}
  {mα : MeasurableSpace α} :
  ⇑(MeasurableEquiv.refl α) = id

Code

lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} :
    (MeasurableEquiv.refl α : α → α) = id

Actions: Source · Open Issue

Proof
rfl