edges_takeUntil_subset — Mathlib

English

Let G be a simple graph on V and p a walk from v to w. If u is a vertex visited by p (u ∈ support(p)), then the edges of the prefix of p up to the first visit to u, denoted by takeUntil, are contained in the edges of p; i.e. (p.takeUntil u h).edges ⊆ p.edges.

Русский

Пусть G — простой граф на V и p — пешеход от v к w. Пусть u — вершина, встречающаяся на p (u ∈ support(p)). Тогда рёбра префикса p до первой встречи вершины u, обозначаемого takeUntil, содержатся в рёбрах p: (p.takeUntil u h).edges ⊆ p.edges.

LaTeX

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

Lean4

theorem edges_takeUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges :=
  List.map_subset _ (p.darts_takeUntil_subset h)

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