map

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

English

Mapping a PMF along the identity yields the same PMF: map id p = p.

Русский

Отображение PMF по тождественному отображению даёт ту же PMF: map id p = p.

LaTeX

$$$\\text{map id } p = p$$$

Lean4

/-- The functorial action of a function on a `PMF`. -/
def map (f : α → β) (p : PMF α) : PMF β :=
  bind p (pure ∘ f)

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

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

Разделы

Аффилиация

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