takeUntil_cons — Mathlib

English

The type of paths between any two vertices is a finite type, as established by the finite walk-length construction.

Русский

Тип путей между двумя вершинами является конечным типом, что следует из конечной длины путей.

LaTeX

$$$\text{Path instFintype}$$$

Lean4

theorem takeUntil_cons {v' : V} {p : G.Walk v' v} (hwp : w ∈ p.support) (h : u ≠ w) (hadj : G.Adj u v') :
    (p.cons hadj).takeUntil w (List.mem_of_mem_tail hwp) = (p.takeUntil w hwp).cons hadj := by simp [Walk.takeUntil, h]

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