image_restrict — Mathlib

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]

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