support_dropUntil_subset — Mathlib

English

The darts (edges) in the initial segment up to u are contained in the darts of the full walk.

Русский

Рёбра в префиксе до u содержатся в рёбрах полного пути.

LaTeX

$$$(p.takeUntil u h).darts \subseteq p.darts$$$

Lean4

theorem support_dropUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.dropUntil u h).support ⊆ p.support := fun x hx =>
  by
  rw [← take_spec p h, mem_support_append_iff]
  exact Or.inr hx

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