LeanMachineLearning exposition

ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr🔗

Minimal Lean file

coe_prodCongr🔗

LemmaProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr.{u_3, u_4, u_5,
    u_6}
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β)
  (e₂ : γ ≃ᵐ δ) : ⇑(MeasurableEquiv.prodCongr e₁ e₂) = Prod.map ⇑e₁ ⇑e₂
ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr.{u_3,
    u_4, u_5, u_6}
  {α : Type u_3} {β : Type u_4}
  {γ : Type u_5} {δ : Type u_6}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β)
  (e₂ : γ ≃ᵐ δ) :
  ⇑(MeasurableEquiv.prodCongr e₁ e₂) =
    Prod.map ⇑e₁ ⇑e₂

Code

lemma MeasurableEquiv.coe_prodCongr {α β γ δ : Type*}
    {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
    {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
    (e₁ : MeasurableEquiv α β) (e₂ : MeasurableEquiv γ δ) :
    (MeasurableEquiv.prodCongr e₁ e₂ : (α × γ) → (β × δ)) = Prod.map e₁ e₂
Used by (1)

Actions: Source · Open Issue

Proof
rfl