length_dropUntil_le — Mathlib

English

If u ∈ support(p), the length of the suffix after dropping until u is at most the length of p: length(p.dropUntil u h) ≤ length(p).

Русский

Если u ∈ поддержка(p), то длина суффикса после удаления до u не превосходит длины p: length(p.dropUntil u h) ≤ length(p).

LaTeX

$$$ (p.dropUntil u h).length \leq p.length $$$

Lean4

theorem length_dropUntil_le {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).length ≤ p.length :=
  by
  have := congr_arg Walk.length (p.take_spec h)
  rw [length_append, add_comm] at this
  exact Nat.le.intro this

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