support_toPath_subset

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

The support of p.toPath is contained in the support 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).support \subseteq p.support$$$

Lean4

theorem support_toPath_subset {u v : V} (p : G.Walk u v) : (p.toPath : G.Walk u v).support ⊆ p.support :=
  support_bypass_subset _

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

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

Разделы

Аффилиация

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