dart_edge_eq_iff — Mathlib

English

Two darts have the same edge iff they are equal or opposite.

Русский

Две стрелы имеют одно и то же ребро тогда и только тогда, когда они равны или противоположны.

LaTeX

$$$ d_1.edge = d_2.edge \iff d_1 = d_2 \lor d_1 = d_2.\text{symm} $$$

Lean4

theorem dart_edge_eq_iff : ∀ d₁ d₂ : G.Dart, d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm :=
  by
  rintro ⟨p, hp⟩ ⟨q, hq⟩
  simp

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