edge_adj — Mathlib

English

For edge s t, the pair (v,w) is adjacent in edge s t exactly when either v=s and w=t (or v=t and w=s) and v ≠ w.

Русский

У ребра s t смежность c вершинами v,w происходит тогда и только тогда, когда либо v=s и w=t (или v=t и w=s) и v ≠ w.

LaTeX

$$$ (\text{edge } s t).\mathrm{Adj}(v,w) \iff \big( (v=s \land w=t) \lor (v=t \land w=s) \big) \land v \neq w $$$

Lean4

theorem edge_adj (v w : V) : (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w := by
  rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]

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