mem_darts_reverse — Mathlib

English

An edge d belongs to the reversed walk's darts iff its symmetric is in the original walk's darts.

Русский

Элемент дротиков обхода в обратном порядке принадлежит обратному обходу тогда и только тогда, когда симметричная пара в исходном обходе.

LaTeX

$$$d \\in p.\\mathrm{reverse}.\\\\darts \\\\iff d^{\\\\mathrm{sym}} \\\\in p.\\\\darts$$$

Lean4

theorem mem_darts_reverse {u v : V} {d : G.Dart} {p : G.Walk u v} : d ∈ p.reverse.darts ↔ d.symm ∈ p.darts := by simp

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