swapRight_zero

Mathlib.Probability.Kernel.Composition.MapComap

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

English

The swapRight operation preserves the zero kernel: applying swapRight to the zero kernel yields the zero kernel.

Русский

Операция swapRight сохраняет нулевое ядро: swapRight 0 = 0.

LaTeX

$$$$swapRight(0) = 0$$$$

Lean4

@[simp]
theorem swapRight_zero : swapRight (0 : Kernel α (β × γ)) = 0 := by simp [swapRight]

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

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

Разделы

Аффилиация

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