prodMkRight_apply

Mathlib.Probability.Kernel.Composition.MapComap

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

English

(prodMkLeft γ κ) ca s = κ (ca.snd) s; i.e., the value on s is κ evaluated at the second component of ca.

Русский

Значение (prodMkLeft γ κ) на (ca, s) равно κ(ca.snd) на s.

LaTeX

$$$ (\operatorname{prodMkLeft} γ κ)\; ca\; s = κ\; ca.snd\; s $$$

Lean4

@[simp]
theorem prodMkRight_apply (κ : Kernel α β) (ca : α × γ) : prodMkRight γ κ ca = κ ca.fst :=
  rfl

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

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

Разделы

Аффилиация

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