map_const — Mathlib

English

For a PMF p and function f, the outer measure of the pushed-forward PMF on a set s equals the outer measure of p on the preimage of s.

Русский

Для PMF p и отображения f внешняя мера образа PMF на множество s равна внешней мере p на предобразе s.

LaTeX

$$$ (p.map f).toOuterMeasure s = p.toOuterMeasure (f^{-1}'s s) $$$

Lean4

@[simp]
theorem map_const : p.map (Function.const α b) = pure b := by
  simp only [map, Function.comp_def, bind_const, Function.const]

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