length_takeUntil_lt — Mathlib

English

If u ≠ w, then the length of the takeUntil prefix is strictly less than the length of p: length(p.takeUntil u h) < length(p).

Русский

Если u ≠ w, тогда длина префикса takeUntil строго меньше длины p.

LaTeX

$$$ (p.takeUntil u h).length < p.length $$$

Lean4

theorem length_takeUntil_lt {u v w : V} {p : G.Walk v w} (h : u ∈ p.support) (huw : u ≠ w) :
    (p.takeUntil u h).length < p.length :=
  by
  rw [(p.length_takeUntil_le h).lt_iff_ne]
  exact fun hl ↦
    huw
      (by
        simpa using
          (hl ▸ getVert_takeUntil h (by rfl) : (p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length))

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