takeUntil — Mathlib

English

If p is a trail and u is in its support, then the prefix of p up to u is a trail.

Русский

Если p — след, и u принадлежит поддержке p, то префикс p до u — след.

LaTeX

$$hc.IsTrail \Rightarrow (p.takeUntil u h).IsTrail$$

Lean4

protected theorem takeUntil {u v w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u ∈ p.support) :
    (p.takeUntil u h).IsTrail :=
  IsTrail.of_append_left (q := p.dropUntil u h) (by rwa [← take_spec _ h] at hc)

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