toMeasure_map — Mathlib

English

If p is a PMF on α and f: α→β is given, then p.toMeasure.map f equals (p.map f).toMeasure when f is measurable.

Русский

Пусть p — PMF на α и f: α→β; p.toMeasure.map f = (p.map f).toMeasure при измеримости f.

LaTeX

$$$ p.toMeasure.map f = (p.map f).toMeasure $$$

Lean4

@[simp]
theorem toMeasure_map (p : PMF α) (hf : Measurable f) : p.toMeasure.map f = (p.map f).toMeasure := by ext s hs : 1;
  rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]

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