adj_edge — Mathlib

English

The adjacency relation on an edge can be expressed through Sym2 as: (edge s t).Adj v w holds iff a certain equality and v ≠ w.

Русский

Смежность на ребре можно записать через Sym2 как: (edge s t).Adj v w выполняется тогда и только тогда, когда выполняется указанное равенство и v ≠ w.

LaTeX

$$$ (\text{edge } s t).Adj v w \iff \big( (\operatorname{Sym2.mk}\{ fst:=s, snd:=t \} = \operatorname{Sym2.mk}\{ fst:=v, snd:=w \}) \big) \land v \neq w $$$

Lean4

theorem adj_edge {v w : V} : (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w :=
  by
  simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, and_congr_left_iff]
  tauto

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