Theorems · Definition · combinatorics

SimpleGraph.Walk.boxProdLeft

{α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} → (H : SimpleGraph β) → {a₁ a₂ : α} → (b : β) → G.Walk a₁ a₂ → (G □ H).Walk (a₁, b) (a₂, b)

Turn a walk on G into a walk on G □ H.

Defined in

Mathlib.Combinatorics.SimpleGraph.Prod

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound