incidence_other_prop — Mathlib

English

The vertex obtained as the other endpoint of an incident edge belongs to the neighbor set of the original vertex.

Русский

Вершина, полученная как другая конечная точка инцидентного ребра, принадлежит множеству соседей исходной вершины.

LaTeX

$$$G.\mathrm{otherVertexOfIncident}(h) \in G.\mathrm{neighborSet}(v).$$$

Lean4

theorem incidence_other_prop {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v) :
    G.otherVertexOfIncident h ∈ G.neighborSet v :=
  by
  obtain ⟨he, hv⟩ := h
  rwa [← Sym2.other_spec' hv, mem_edgeSet] at he

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