append_nil

Mathlib.Combinatorics.SimpleGraph.Walk

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

← MathLib Explorer

English

Appending an empty walk nil to any walk p yields p itself: p.append nil = p.

Русский

Прицепление пустого пути nil к пути p не меняет путь: p.append nil = p.

LaTeX

$$$$\forall {u,v} (p : G.Walk u v),\ p.append(\text{nil}) = p.$$$$

Lean4

@[simp]
theorem append_nil {u v : V} (p : G.Walk u v) : p.append nil = p := by
  induction p with
  | nil => rw [nil_append]
  | cons _ _ ih => rw [cons_append, ih]

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

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

Разделы

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

Аффилиация

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