support_append

Mathlib.Combinatorics.SimpleGraph.Walk

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

← MathLib Explorer

English

The support of p.append p' is the support of p followed by the tail of p'.

Русский

Опора p.append p' равна опоре p плюс хвост опоры p'.

LaTeX

$$$ (p.\append p').\mathrm{support} = p.\mathrm{support} \; \cup \; p'.\mathrm{support}.\mathrm{tail} $$$

Lean4

theorem support_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support = p.support ++ p'.support.tail := by induction p <;> cases p' <;> simp [*]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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