prodMkLeft_apply'

Mathlib.Probability.Kernel.Composition.MapComap

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

English

(prodMkRight γ κ) ca s = κ (ca.fst) s; i.e., the value on s is κ evaluated at the first component of ca.

Русский

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

LaTeX

$$$ (\operatorname{prodMkRight} γ κ)\; ca\; s = κ\; ca.fst\; s $$$

Lean4

theorem prodMkLeft_apply' (κ : Kernel α β) (ca : γ × α) (s : Set β) : prodMkLeft γ κ ca s = κ ca.snd s :=
  rfl

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

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

Разделы

Аффилиация

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