map_comp

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.map_comp

English

Composition of maps corresponds to mapping with the composed function: (p.map f).map g = p.map (g ∘ f).

Русский

Сцепление отображений соответствует отображению по композиции: (p.map f).map g = p.map (g ∘ f).

LaTeX

$$$\\text{map } g (\\text{map } f (p)) = \\text{map } (g \\circ f) (p)$$$

Lean4

theorem map_comp (g : β → γ) : (p.map f).map g = p.map (g ∘ f) := by simp [map, Function.comp_def]

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

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

Разделы

Аффилиация

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