LeanMachineLearning exposition

ProbabilityTheory.Kernel.prodMkLeft_inj🔗

Minimal Lean file

prodMkLeft_inj🔗

LemmaProbabilityTheory.Kernel.prodMkLeft_inj
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkLeft_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 α β) :
  prodMkLeft γ κ = prodMkLeft γ ν ↔ κ = ν
ProbabilityTheory.Kernel.prodMkLeft_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 α β) :
  prodMkLeft γ κ = prodMkLeft γ ν ↔ κ = ν

Code

lemma prodMkLeft_inj [h_nonempty : Nonempty γ]
    (κ ν : Kernel α β) :
    κ.prodMkLeft γ = ν.prodMkLeft γ ↔ κ = ν
Used by (1)

Actions: Source · Open Issue

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