comp_zero

Mathlib.Probability.Kernel.Composition.Comp

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

English

Composition with the zero kernel on the other side yields zero: κ ∘ₖ (0 : Kernel α β) = 0.

Русский

Слeжение с нулевым ядром с другой стороны даёт ноль: κ ∘ₖ 0 = 0.

LaTeX

$$$\\kappa \\circ_k (0 : \\text{Kernel } \\alpha \\beta) = 0$$$

Lean4

@[simp]
theorem comp_zero (κ : Kernel β γ) : κ ∘ₖ (0 : Kernel α β) = 0 := by ext; simp [comp_apply]

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

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

Разделы

Аффилиация

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