darts_dropUntil_subset — Mathlib

English

The set of darts after removing up to a vertex is contained in the darts of the original walk.

Русский

Множество рёбер после удаления до вершины содержится в рёбрах исходного пути.

LaTeX

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

Lean4

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

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