graph_injective — Mathlib

English

The graph operator is injective: if f.graph = g.graph then f = g.

Русский

Оператор графа инъективен: если графы функций совпадают, то сами функции равны.

LaTeX

$$$\\text{Injective}(\\mathrm{graph})$ for finsupp$$

Lean4

theorem graph_injective (α M) [Zero M] : Injective (@graph α M _) :=
  by
  intro f g h
  classical
  have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
  refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
  exact mk_mem_graph _ (hsup ▸ hx)

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