drop_support_eq_support_drop_min — Mathlib

English

Let p be a walk and n a natural number. Then the support after dropping the first n vertices equals the original support with the first min(n, length(p)) elements removed: (p.drop n).support = p.support.drop(min(n, p.length)).

Русский

Пусть p — ход, n — натуральное число. Тогда опора после удаления первых n вершин равна исходной опоре с удалением первых min(n, length(p)) элементов: (p.drop n).support = p.support.drop(min(n, p.length)).

LaTeX

$$$ (p.drop n).\\support = p.support.drop(\\min(n, p.length)) $$$

Lean4

theorem drop_support_eq_support_drop_min {u v} (p : G.Walk u v) (n : ℕ) :
    (p.drop n).support = p.support.drop (n ⊓ p.length) := by
  induction p generalizing n with
  | nil => simp [drop]
  | cons => cases n <;> simp_all [drop]

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