incidence_other_neighbor_edge — Mathlib

English

There is a natural bijection between the edges incident to a vertex v and the vertices adjacent to v, given by sending an edge to its other endpoint and conversely sending a neighbor to the edge {v, neighbor}.

Русский

Существует естественная биекция между множеством рёбер, инцидентных вершине v, и множеством соседей вершины v: ребро отображаетcя в другой конец ребра; сосед отображается в ребро {v, neighbor}.

LaTeX

$$$\mathrm{Incidence}_G(v) \cong G.\mathrm{neighborSet}(v).$$$

Lean4

@[simp]
theorem incidence_other_neighbor_edge {v w : V} (h : w ∈ G.neighborSet v) :
    G.otherVertexOfIncident (G.mem_incidence_iff_neighbor.mpr h) = w :=
  Sym2.congr_right.mp (Sym2.other_spec' (G.mem_incidence_iff_neighbor.mpr h).right)

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