take_support_eq_support_take_succ

English

Let p be a walk from u to v in G and n a natural number. Then the support of the prefix of length n is exactly the first n+1 elements of the walk's support: (p.take n).support = p.support.take(n+1).

Русский

Пусть p — ход графа G от вершины u к вершине v и n ∈ ℕ. Тогда опора префикса длины n равна первым n+1 элементам опоры графа: (p.take n).support = p.support.take(n+1).

LaTeX

$$$ (p.take n).support = p.support.take(n + 1) $$$

Lean4

theorem take_support_eq_support_take_succ {u v} (p : G.Walk u v) (n : ℕ) :
    (p.take n).support = p.support.take (n + 1) := by
  induction p generalizing n with
  | nil => simp [take]
  | cons => cases n <;> simp_all [take]

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