dart_edge_eq_mk'_iff — Mathlib

English

An edge equals Sym2.mk p exactly when the underlying endpoints are p or p swapped.

Русский

Ребро равно Sym2.mk p тогда, когда концы стрелы равны p или p поменяны местами.

LaTeX

$$$ d.edge = Sym2.mk p \iff d.toProd = p \lor d.toProd = p.swap $$$

Lean4

theorem dart_edge_eq_mk'_iff : ∀ {d : G.Dart} {p : V × V}, d.edge = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = p.swap :=
  by
  rintro ⟨p, h⟩
  apply Sym2.mk_eq_mk_iff

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