Lemmas about map and comap of Markov kernels

@[simp]

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

@[simp]

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

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_deterministic {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) : prodMkLeft γ (deterministic f hf) = deterministic (fun (p : γ × α) => f p.2) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_deterministic {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) : prodMkRight γ (deterministic f hf) = deterministic (fun (p : α × γ) => f p.1) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.comap_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (ν : MeasureTheory.Measure β) {f : α → γ} (hf : Measurable f) : (const γ ν).comap f hf = const α ν