Theorems · Definition · combinatorics

SimpleGraph.ConnectedComponent.recOn

{V : Type u} →
  {G : SimpleGraph V} →
    {motive : G.ConnectedComponent → Sort u_1} →
      (c : G.ConnectedComponent) →
        (f : (v : V) → motive (G.connectedComponentMk v)) →
          (∀ (u v : V) (p : G.Walk u v), p.IsPath → ⋯ ▸ f u = f v) → motive c

This is Quot.recOn specialized to connected components. For convenience, it strengthens the assumptions in the hypothesis to provide a path between the vertices.

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound