graph_eq_empty — Mathlib

English

For every finitely supported function f : α →₀ M, the graph of f is empty if and only if f is the zero function.

Русский

Для любого f : α →₀ M граф f равен пустому множеству тогда и только тогда, когда f равно нулю.

LaTeX

$$$\\forall f:\\alpha \\to_0 M,\\; f.graph = \\emptyset \\iff f = 0$$$

Lean4

@[simp]
theorem graph_eq_empty {f : α →₀ M} : f.graph = ∅ ↔ f = 0 :=
  (graph_injective α M).eq_iff' graph_zero

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