English
Let G be a simple graph on vertex set V. For a vertex v and an edge e incident to v, the value of the auxiliary function otherVertexOfIncident at the witness h ∈ e ∈ incidenceSet(v) is the other endpoint of e.
Русский
Пусть G — простой граф на множестве вершин V. Для вершины v и ребра e, инцидентного v, значение функции-помощника otherVertexOfIncident, применённой к доказательству h ∈ incidenceSet(v), равно другой концe ребра e.
LaTeX
$$$\forall v \in V, \forall e \in \mathrm{Sym}^2 V, \forall h \ (e \in \mathrm{incidenceSet}_G(v) \Rightarrow e = \{v, G.\text{otherVertexOfIncident}(h)\}).$$$
Lean4
/-- Given an edge incident to a particular vertex, get the other vertex on the edge. -/
def otherVertexOfIncident {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v) : V :=
Sym2.Mem.other' h.2
