getVert_takeUntil — Mathlib

English

Let u,v be vertices and n a natural number. If w ∈ support(p) and n ≤ length(p.takeUntil w hw), then the vertex at position n in p.takeUntil w hw equals the vertex at position n in p: (p.takeUntil w hw).getVert n = p.getVert n.

Русский

Пусть u,v — вершины, n — число. Если w ∈ support(p) и n ≤ length(p.takeUntil w hw), то n-ая вершина в p.takeUntil w hw равна n-ой вершине в p: (p.takeUntil w hw).getVert n = p.getVert n.

LaTeX

$$$ (p.takeUntil w hw).getVert n = p.getVert n $$$

Lean4

theorem getVert_takeUntil {u v : V} {n : ℕ} {p : G.Walk u v} (hw : w ∈ p.support) (hn : n ≤ (p.takeUntil w hw).length) :
    (p.takeUntil w hw).getVert n = p.getVert n :=
  by
  conv_rhs => rw [← take_spec p hw, getVert_append]
  cases hn.lt_or_eq <;> simp_all

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