getVert_length_takeUntil

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp

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

Lean4

theorem getVert_length_takeUntil {p : G.Walk v w} (h : u ∈ p.support) : p.getVert (p.takeUntil _ h).length = u :=
  by
  have := congr_arg₂ (y := (p.takeUntil _ h).length) getVert (p.take_spec h) rfl
  grind [getVert_append, getVert_zero]

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

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

Разделы

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

Аффилиация

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