darts_toPath_subset

Mathlib.Combinatorics.SimpleGraph.Paths

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.darts_toPath_subset

English

The darts of p.toPath are contained in the darts of p.

Русский

Дартсы p.toPath содержатся в дартс(p).

LaTeX

$$$ \forall {V} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v), (p.toPath : G.Walk u v).darts \subseteq p.darts$$$

Lean4

theorem darts_toPath_subset {u v : V} (p : G.Walk u v) : (p.toPath : G.Walk u v).darts ⊆ p.darts :=
  darts_bypass_subset _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru