English
For countable ι with Directed-on-subset structure, the restriction to the union equals the iSup of the restrictions on each s i.
Русский
При счётном ι с направленной по включению структурой ограничение на объединение равно iSup ограничений по каждому s_i.
LaTeX
$$$[Countable\, ι] \ (Directed (\subseteq) s) \Rightarrow \mu.restrict (\bigcup i, s i) = \bigl(\bigsqcup_i \mu.restrict (s i)\bigr)$$$
Lean4
/-- The restriction of the pushforward measure is the pushforward of the restriction. For a version
assuming only `AEMeasurable`, see `restrict_map_of_aemeasurable`. -/
theorem restrict_map {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
(μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
ext fun t ht => by simp [*, hf ht]
