instIsCondKernel_zero

Mathlib.Probability.Kernel.Disintegration.Basic

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

English

The zero kernel is a CondKernel for any κCond with trivial disintegration.

Русский

Нуль-ядро является CondKernel для любого κCond с тривиальным разложением.

LaTeX

$$$IsCondKernel 0 \\; \\kappaCond$$$

Lean4

instance instIsCondKernel_zero (κCond : Kernel (α × β) Ω) : IsCondKernel 0 κCond where disintegrate := by simp

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

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

Разделы

Аффилиация

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