prod_of_not_isSFiniteKernel_right

Mathlib.Probability.Kernel.Composition.Prod

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

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_right (κ : Kernel α β) {η : Kernel α γ} (h : ¬IsSFiniteKernel η) : κ ×ₖ η = 0 := by
  simp [prod, h]

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

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

Разделы

Аффилиация

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