length_takeUntil_le — Mathlib

English

If u ∈ support(p), then the length of the prefix taken until u is no greater than the length of p: length(p.takeUntil u h) ≤ length(p).

Русский

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

LaTeX

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

Lean4

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

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