mem_graph_snd_inj' — Mathlib

English

The graph of -f is the pushforward of the graph of f by the pair of maps (id_E, -id_F).

Русский

Граф -f является отображением графа f через пару отображений (id_E, -id_F).

LaTeX

$$$(-f).graph = f.graph.map\left( (\mathrm{id}_E, -\mathrm{id}_F) \right).$$$

Lean4

theorem mem_graph_snd_inj' (f : E →ₗ.[R] F) {x y : E × F} (hx : x ∈ f.graph) (hy : y ∈ f.graph) (hxy : x.1 = y.1) :
    x.2 = y.2 := by
  cases x
  cases y
  exact f.mem_graph_snd_inj hx hy hxy

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