English
For a measurable s, membership of r in the range of restrict f s is characterized by r = 0 with s ≠ univ or r ∈ f '' s.
Русский
Для измеримого s членство в диапазоне restrict f s эквивалентно либо r = 0 и s ≠ univ, либо r ∈ f '' s.
LaTeX
$$$r \\in (\\restrict f s).range \\iff (r = 0 \\land s \\neq \\mathrm{univ}) \\lor r \\in f''s.$$$
Lean4
theorem map_restrict_of_zero [Zero γ] {g : β → γ} (hg : g 0 = 0) (f : α →ₛ β) (s : Set α) :
(f.restrict s).map g = (f.map g).restrict s :=
ext fun x =>
if hs : MeasurableSet s then by simp [hs, Set.indicator_comp_of_zero hg]
else by simp [restrict_of_not_measurable hs, hg]