mem_image_of_mem_range_restrict — Mathlib

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

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