LeanMachineLearning exposition

ProbabilityTheory.identDistrib_comm🔗

Minimal Lean file

identDistrib_comm🔗

LemmaProbabilityTheory.identDistrib_comm
Details

No docstring.

🔗theorem
ProbabilityTheory.identDistrib_comm.{u_2, u_3, u_4} {Ω : Type u_2}
  {Ω' : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'} {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure Ω} (X : Ω → E) (Y : Ω' → E)
  {ν : MeasureTheory.Measure Ω'} :
  IdentDistrib X Y μ ν ↔ IdentDistrib Y X ν μ
ProbabilityTheory.identDistrib_comm.{u_2,
    u_3, u_4}
  {Ω : Type u_2} {Ω' : Type u_3}
  {E : Type u_4} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure Ω}
  (X : Ω → E) (Y : Ω' → E)
  {ν : MeasureTheory.Measure Ω'} :
  IdentDistrib X Y μ ν ↔
    IdentDistrib Y X ν μ

Code

lemma identDistrib_comm (X : Ω → E) (Y : Ω' → E) {ν : Measure Ω'} :
    IdentDistrib X Y μ ν ↔ IdentDistrib Y X ν μ
Used by (1)

Actions: Source · Open Issue

Proof
⟨fun h ↦ h.symm, fun h ↦ h.symm⟩