parallelComp_of_not_isSFiniteKernel_right

Mathlib.Probability.Kernel.Composition.ParallelComp

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

← MathLib Explorer

English

If η is not SFinite, then κ ∥ₖ η = 0 for any κ.

Русский

Если η не SFinite, то κ ∥ₖ η = 0 для любого κ.

LaTeX

$$$\\text{parallelComp}(\\kappa, \\eta) = 0$ if $\\lnot \\text{IsSFiniteKernel}(\\eta)$$$

Lean4

@[simp]
theorem parallelComp_of_not_isSFiniteKernel_right (κ : Kernel α β) (h : ¬IsSFiniteKernel η) : κ ∥ₖ η = 0 := by
  rw [parallelComp, dif_neg (not_and_of_not_right _ h)]

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

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

Разделы

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

Аффилиация

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