map_restrict_of_zero — Mathlib

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]

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