English
The image of the restricted function equals the image of the intersection under f.
Русский
Образ ограниченной функции равен образу пересечения через f.
LaTeX
$$$\operatorname{image}(\operatorname{restrict}(f), \operatorname{preimage} \operatorname{Subtype.val} (t)) = \operatorname{image}(f, t \cap s)$$$
Lean4
theorem image_restrict (f : α → β) (s t : Set α) : s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s) := by
rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]