sectR_zero

Mathlib.Probability.Kernel.Composition.MapComap

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

English

The sectR construction preserves the zero kernel: for any a, sectR (0 : Kernel (α × β) γ) a = 0.

Русский

Конструкция sectR сохраняет нуль-ядро: для любого a секция sectR(0) a = 0.

LaTeX

$$sectR (0 : Kernel (α × β) γ) a = 0$$

Lean4

@[simp]
theorem sectR_zero (a : α) : sectR (0 : Kernel (α × β) γ) a = 0 := by simp [sectR]

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

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

Разделы

Аффилиация

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