fst_compProd

Mathlib.Probability.Kernel.Composition.CompProd

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

← MathLib Explorer

English

The first marginal of the product kernel satisfies fst (κ ⊗ η) = κ.

Русский

Первая маргинальная часть произведения ядер равна κ.

LaTeX

$$$$ \\text{fst}(κ ⊗_{\\kern-0.2em} η) = κ.$$$$

Lean4

@[simp]
theorem fst_compProd (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] :
    fst (κ ⊗ₖ η) = κ := by ext x s hs; simp [fst_compProd_apply, hs]

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

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

Разделы

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

Аффилиация

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