recOn

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.recOn

Lean4

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def recOn {motive : G.ConnectedComponent → Sort*} (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath), ConnectedComponent.sound p.reachable ▸ f u = f v) : motive c :=
  Quot.recOn c f fun u v r => r.elim_path fun p => h u v p p.2

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

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

Разделы

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

Аффилиация

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