prodMkLeft_apply

Mathlib.Probability.Kernel.Composition.MapComap

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

English

Applying prodMkLeft to a pair (c, a) yields κ applied to a; i.e., (prodMkLeft γ κ)(c, a) = κ(a).

Русский

Применение prodMkLeft к паре (c, a) даёт κ(a).

LaTeX

$$$ (\operatorname{prodMkLeft} γ κ)(c, a) = κ(a) $$$

Lean4

@[simp]
theorem prodMkLeft_apply (κ : Kernel α β) (ca : γ × α) : prodMkLeft γ κ ca = κ ca.snd :=
  rfl

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

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

Разделы

Аффилиация

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