image_image_val_eq_restrict_image

English

The image of a set under a function is equal to the image of that set under the restricted function to a subset.

Русский

Образ множества через функцию равен образу множества через ограниченную на подмножество функцию.

LaTeX

$$$\operatorname{image} f (\gamma) = \operatorname{image} (\beta \restriction f) \gamma.$$$

Lean4

theorem image_image_val_eq_restrict_image {δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ := by ext; simp

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