takeUntil_first

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp

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

English

The initial segment of a walk before its starting vertex is empty.

Русский

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

LaTeX

$$p.takeUntil u p.start_mem_support = .nil$$

Lean4

@[simp]
theorem takeUntil_first (p : G.Walk u v) : p.takeUntil u p.start_mem_support = .nil := by
  cases p <;> simp [Walk.takeUntil]

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

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

Разделы

Аффилиация

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