cons_map_snd_darts — Mathlib

English

Membership of a reversed walk's darts corresponds to membership of the symmetric of the original's darts.

Русский

Членство в дротиках обращения соответствует членству симметричной пары дротиков исходного обхода.

LaTeX

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

Lean4

theorem cons_map_snd_darts {u v : V} (p : G.Walk u v) : (u :: p.darts.map (·.snd)) = p.support := by
  induction p <;> simp! [*]

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