range_restrict — Mathlib

English

Let f: A → B and sets S ⊆ A, T ⊆ B with f[S] ⊆ T. Then the range of the restricted map f|S→T equals the set of all y ∈ T that occur as f(x) for some x ∈ S.

Русский

Пусть f: A→B и множества S ⊆ A, T ⊆ B таковы, что f(S) ⊆ T. Тогда образ ограниченного отображения f|S→T равен множеству всех y ∈ T, которые равны f(x) для некоторого x ∈ S.

LaTeX

$$$\operatorname{range}(f\restriction s\, t) = \operatorname{Subtype.val}^{-1}\big(\operatorname{image}(f, s)\big)$$$

Lean4

theorem range_restrict (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) :
    range (h.restrict f s t) = Subtype.val ⁻¹' (f '' s) :=
  Set.range_subtype_map f h

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