snd_compProd

Mathlib.Probability.Kernel.Composition.MeasureComp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.snd_compProd

Lean4

@[simp]
theorem snd_compProd (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ] : (μ ⊗ₘ κ).snd = κ ∘ₘ μ :=
  by
  ext s hs
  rw [bind_apply hs κ.aemeasurable, snd_apply hs, compProd_apply]
  · rfl
  · exact measurable_snd hs

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru