graph_eq_ker_coprod — Mathlib

English

There is a relation expressing the graph of a map g as the kernel of a certain coproduct construction: graph(g) = ker((-g) ∘coprod id).

Русский

Существует связь: граф отображения g равен ядру оператора вида (-g) coprod id, т.е. граф равен ядру соответствующего копредприятия.

LaTeX

$$$\\text{graph}(g) = \\ker\\big((-g) \\\\mathrm{coprod} \\mathrm{id}\\big)$$$

Lean4

theorem graph_eq_ker_coprod : g.graph = ker ((-g).coprod LinearMap.id) :=
  by
  ext x
  change _ = _ ↔ -g x.1 + x.2 = _
  rw [add_comm, add_neg_eq_zero]

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