English
An element (a,m) belongs to the graph of f iff f(a)=m and m≠0.
Русский
Элемент $(a,m)$ принадлежит графу функции f тогда и только тогда, когда $f(a)=m$ и $m\\neq 0$.
LaTeX
$$$(a,m) \\in f.graph \\iff f(a) = m \\land m \\neq 0$$$
Lean4
theorem mk_mem_graph_iff {a : α} {m : M} {f : α →₀ M} : (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0 :=
by
simp_rw [graph, mem_map, mem_support_iff]
constructor
· rintro ⟨b, ha, rfl, -⟩
exact ⟨rfl, ha⟩
· rintro ⟨rfl, ha⟩
exact ⟨a, ha, rfl⟩