edge_other_incident_set — Mathlib

English

If e is incident to a vertex v, then e is also incident to the other endpoint of e, namely G.otherVertexOfIncident(h).

Русский

Если e инцидентно вершине v, то e также инцидентно другой конечной вершине e, то есть G.otherVertexOfIncident(h).

LaTeX

$$$\forall v, e, h\ (e \in \mathrm{incidenceSet}_G(v) \Rightarrow e \in \mathrm{incidenceSet}_G(G.\mathrm{otherVertexOfIncident}(h))).$$$

Lean4

theorem edge_other_incident_set {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v) :
    e ∈ G.incidenceSet (G.otherVertexOfIncident h) := by
  use h.1
  simp [otherVertexOfIncident, Sym2.other_mem']

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