English
If u ∈ support(p) and n ≤ (p.takeUntil w hw).length, then p.getVert n = u implies something about the position n relative to the length (theorem provides a biconditional with length). In particular, a strict bound on n relates to the occurrence of u.
Русский
Если u ∈ support(p) и n ≤ (p.takeUntil w hw).length, то p.getVert n = u эквивалентно отношению n к длине префикса; точнее: существует эквивалентность, связывающая значение p.getVert n и длину takeUntil.
LaTeX
$$$$ p.getVert n = u \iff n = (p.takeUntil w hw).length \text{ при } n \le (p.takeUntil w hw).length $$$$
Lean4
theorem getVert_lt_length_takeUntil_ne {n : ℕ} {p : G.Walk v w} (h : u ∈ p.support)
(hn : n < (p.takeUntil _ h).length) : p.getVert n ≠ u :=
by
rintro rfl
have h₁ : n < (p.takeUntil _ h).support.dropLast.length := by simpa
have : p.getVert n ∈ (p.takeUntil _ h).support.dropLast := by
simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le, ← List.getElem_dropLast h₁,
List.getElem_mem h₁]
have := support_eq_concat _ ▸ p.count_support_takeUntil_eq_one h
grind [List.not_mem_of_count_eq_zero]
