LeanMachineLearning exposition

ProbabilityTheory.Kernel.prodMkRight_inj🔗

Minimal Lean file

prodMkRight_inj🔗

LemmaProbabilityTheory.Kernel.prodMkRight_inj
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkRight_inj.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ] (κ ν : Kernel α β) :
  prodMkRight γ κ = prodMkRight γ ν ↔ κ = ν
ProbabilityTheory.Kernel.prodMkRight_inj.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ]
  (κ ν : Kernel α β) :
  prodMkRight γ κ = prodMkRight γ ν ↔
    κ = ν

Code

lemma prodMkRight_inj [h_nonempty : Nonempty γ]
    (κ ν : Kernel α β) :
    κ.prodMkRight γ = ν.prodMkRight γ ↔ κ = ν

Actions: Source · Open Issue

Proof
by
  simp only [Kernel.ext_iff, Kernel.prodMkRight_apply, Prod.forall]
  exact ⟨fun h a ↦ h a h_nonempty.some, fun h a _ ↦ h a⟩