takeUntil

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp

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

Lean4

/-- Given a vertex in the support of a path, give the path up until (and including) that vertex. -/
def takeUntil {v w : V} : ∀ (p : G.Walk v w) (u : V), u ∈ p.support → G.Walk v u
  | nil, u, h => by rw [mem_support_nil_iff.mp h]
  | cons r p, u, h =>
    if hx : v = u then hx ▸ Walk.nil
    else
      cons r
        (takeUntil p u <| by
          cases h
          · exact (hx rfl).elim
          · assumption)

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

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

Разделы

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

Аффилиация

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