sectR_swapRight

Mathlib.Probability.Kernel.Composition.MapComap

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

English

Symmetrically, sectR (swapLeft κ) = sectL κ for any κ.

Русский

Аналогично, sectR (swapLeft κ) = sectL κ.

LaTeX

$$sectR (swapLeft κ) = sectL κ$$

Lean4

@[simp]
theorem sectR_swapRight (κ : Kernel (α × β) γ) : sectR (swapLeft κ) = sectL κ :=
  rfl

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

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

Разделы

Аффилиация

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