pure_map — Mathlib

English

Let f: α → β. If p is the Dirac PMF concentrated at a, then the image under f is the Dirac PMF concentrated at f(a).

Русский

Пусть f : α → β. Пусть PMF имеет единичную массу в элементе a; отображение через f приводит к единичной массе в элементе f(a).

LaTeX

$$$ PMF.map f (PMF.pure a) = PMF.pure (f a) $$$

Lean4

theorem pure_map (a : α) : (pure a).map f = pure (f a) :=
  pure_bind _ _

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