edge_other_ne — Mathlib

English

If e ∈ E(G) and v ∈ e, then the other endpoint of v in e is different from v.

Русский

Если e ∈ E(G) и v ∈ e, то другая вершина конца ребра e не равна v.

LaTeX

$$$$ \forall e \in E(G),\ \forall v \in e,\ \mathrm{other}(v,e) \neq v. $$$$

Lean4

theorem edge_other_ne {e : Sym2 V} (he : e ∈ G.edgeSet) {v : V} (h : v ∈ e) : Sym2.Mem.other h ≠ v :=
  by
  rw [← Sym2.other_spec h, Sym2.eq_swap] at he
  exact G.ne_of_adj he

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