compProd_of_not_isSFiniteKernel_right

Mathlib.Probability.Kernel.Composition.CompProd

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

← MathLib Explorer

English

If the kernel η is not S-finite, then κ ⊗ₖ η equals the zero kernel for any κ.

Русский

Если ядро η не S-конечное, то произведение κ ⊗ₖ η равно нулю для любого κ.

LaTeX

$$$$\kappa \otimes_k \eta = 0,$$$$

Lean4

@[simp]
theorem compProd_of_not_isSFiniteKernel_right (κ : Kernel α β) (η : Kernel (α × β) γ) (h : ¬IsSFiniteKernel η) :
    κ ⊗ₖ η = 0 := by simp [compProd, h]

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

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

Разделы

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

Аффилиация

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