zero_comp

Mathlib.Probability.Kernel.Composition.Comp

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

English

Composition with the zero kernel yields the zero kernel: (0 : Kernel β γ) ∘ₖ κ = 0.

Русский

Сложение с нулевым ядром даёт нулевое ядро: (0 : Kernel β γ) ∘ₖ κ = 0.

LaTeX

$$$\\bigl(0 : \\text{Kernel } \\beta \\gamma\\bigr) \\circ_k \\kappa = 0$$$

Lean4

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

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

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

Разделы

Аффилиация

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