English
Taking until w on p and then until x on the result equals taking until x on p with an appropriate subset of the support: (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx).
Русский
Применение takeUntil до w, затем до x на результате, эквивалентно takeUntil до x на исходном p с соответствующей подмножностью поддержки: (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx).
LaTeX
$$$$ (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx) $$$$
Lean4
/-- Given a walk `p` and a node in the support, there exists a natural `n`, such that given node
is the `n`-th node (zero-indexed) in the walk. In addition, `n` is at most the length of the walk.
Due to the definition of `getVert` it would otherwise be legal to return a larger `n` for the last
node. -/
theorem mem_support_iff_exists_getVert {u v w : V} {p : G.Walk v w} :
u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length := by
classical
exact
Iff.intro (fun h ↦ ⟨_, p.getVert_length_takeUntil h, p.length_takeUntil_le h⟩)
(fun ⟨_, h, _⟩ ↦ h ▸ getVert_mem_support _ _)
