edges_dropUntil_subset — Mathlib

English

Let p be a walk and u ∈ support(p). Then the edges of the suffix obtained by dropping up to u, i.e. (p.dropUntil u h).edges, are contained in p.edges.

Русский

Пусть p — пешеход, и u ∈ поддержка(p). Тогда рёбра суффикса, полученного после удаления до u, то есть (p.dropUntil u h).edges, содержатся в p.edges.

LaTeX

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

Lean4

theorem edges_dropUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges :=
  List.map_subset _ (p.darts_dropUntil_subset h)

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