compProd_fst_condKernelReal

Mathlib.Probability.Kernel.Disintegration.StandardBorel

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.compProd_fst_condKernelReal

← MathLib Explorer

English

The composition of the first projection and condKernelReal κ equals κ.

Русский

Составление проекции fst и condKernelReal κ равно κ.

LaTeX

$$$\fst\kappa \circ \mathrm{condKernelReal}(\kappa) = \kappa$$$

Lean4

theorem compProd_fst_condKernelReal (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : fst κ ⊗ₖ condKernelReal κ = κ := by
  rw [condKernelReal, compProd_toKernel]

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

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

Разделы

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

Аффилиация

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