take_getVert

Mathlib.Combinatorics.SimpleGraph.Walk

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

← MathLib Explorer

English

For all p, n, m, the m-th vertex of p.take n equals p.getVert (min(n,m)).

Русский

Для всех p, n, m вершина m в p.take n равна p.getVert(min(n,m)).

LaTeX

$$$ (p.take n).getVert m = p.getVert (\min(n,m)) $$$

Lean4

@[simp]
theorem take_getVert (p : G.Walk u v) (n m : ℕ) : (p.take n).getVert m = p.getVert (n ⊓ m) := by
  induction p generalizing n m with
  | nil => simp [take]
  | cons => cases n <;> cases m <;> simp_all [take]

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

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

Разделы

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

Аффилиация

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