mk_mem_graph_iff — Mathlib

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⟩

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