English
Let f be a linear partial map from E to F. An element y ∈ F lies in the image of f if and only if there exists x ∈ E such that (x, y) belongs to the graph of f.
Русский
Пусть f — линейное частичное отображение из E в F. Элемент y ∈ F принадлежит образу f тогда и только тогда, когда существует x ∈ E такое, что пара (x, y) принадлежит графику f.
LaTeX
$$$ y \\in \\operatorname{range}(f) \\iff \\exists x \\in E,\\ (x, y) \\in \\operatorname{graph}(f) $$$
Lean4
theorem mem_range_iff {f : E →ₗ.[R] F} {y : F} : y ∈ Set.range f ↔ ∃ x : E, (x, y) ∈ f.graph :=
by
constructor <;> intro h
· rw [Set.mem_range] at h
rcases h with ⟨⟨x, hx⟩, h⟩
use x
rw [← h]
exact f.mem_graph ⟨x, hx⟩
grind [mem_graph_iff]
