English
Let f be a simple function with values in β and let s be a subset of α. If a nonzero value r lies in the range of the restriction of f to s, then r is actually attained by f on some point of s; equivalently, r ∈ f''s.
Русский
Пусть f — простая функция с значениями в β и пусть s ⊆ α. Если не нулевое значение r встречается в диапазоне ограниченной функции f на s, то это значение принадлежит образу f на множестве s; то есть r ∈ f '' s.
LaTeX
$$$ (r \in (\operatorname{restrict} f s).\operatorname{range}) \land r \neq 0 \Rightarrow r \in f''s $$$
Lean4
theorem mem_image_of_mem_range_restrict {r : β} {s : Set α} {f : α →ₛ β} (hr : r ∈ (restrict f s).range) (h0 : r ≠ 0) :
r ∈ f '' s :=
if hs : MeasurableSet s then by simpa [mem_restrict_range hs, h0, -mem_range] using hr
else by
rw [restrict_of_not_measurable hs] at hr
exact (h0 <| eq_zero_of_mem_range_zero hr).elim