prod_of_not_isSFiniteKernel_left

Mathlib.Probability.Kernel.Composition.Prod

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

English

If κ is not s-finite, then κ.prod η = 0.

Русский

Если κ не s-конечное, то κ.prod η = 0.

LaTeX

$$$$Not(IsSFiniteKernel κ) \\Rightarrow κ.prod η = 0.$$$$

Lean4

@[simp]
theorem prod_of_not_isSFiniteKernel_left {κ : Kernel α β} (η : Kernel α γ) (h : ¬IsSFiniteKernel κ) : κ ×ₖ η = 0 := by
  simp [prod, h]

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

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

Разделы

Аффилиация

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