darts_takeUntil_subset — Mathlib

English

The darts in the portion after dropping until u are contained in the full walk's darts.

Русский

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

LaTeX

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

Lean4

theorem darts_takeUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).darts ⊆ p.darts :=
  fun x hx => by
  rw [← take_spec p h, darts_append, List.mem_append]
  exact Or.inl hx

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