image_iff — Mathlib

English

For f: E →ₗ.[R] F and x ∈ E, y ∈ F, y = f(x) if and only if (x,y) ∈ graph(f) (provided x ∈ dom f).

Русский

Для f: E →ₗ.[R] F и x ∈ E, y ∈ F, y = f(x) тогда и только тогда, когда (x,y) принадлежит графу f (при условии x ∈ dom f).

LaTeX

$$$\forall x:\, x \in \operatorname{dom}(f) \Rightarrow (y=f(x) \iff (x,y) \in \mathrm{graph}(f)).$$$

Lean4

theorem image_iff {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x ∈ f.domain) : y = f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph := by
  grind [mem_graph_iff]

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