getVert_reverse — Mathlib

English

The i-th vertex of p.reverse is the (length(p) - i)-th vertex of p.

Русский

i-я вершина обращения p.reverse равна (length(p) - i)-й вершине p.

LaTeX

$$$p.reverse.getVert(i) = p.getVert(p.length - i)$$$

Lean4

theorem getVert_reverse {u v : V} (p : G.Walk u v) (i : ℕ) : p.reverse.getVert i = p.getVert (p.length - i) := by
  induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
    split_ifs
    next hi =>
      rw [Nat.succ_sub hi.le]
      simp [getVert]
    next hi =>
      obtain rfl | hi' := eq_or_gt_of_not_lt hi
      · simp
      · rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp [getVert]

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