Theorems · Theorem · combinatorics

SimpleGraph.Walk.map_mapToSubgraph_eq_induce

∀ {V : Type u} {G : SimpleGraph V} (s : Set V) {u v : V} (w : G.Walk u v) (hs : ∀ x ∈ w.support, x ∈ s),
  SimpleGraph.Walk.map { toFun := fun x => ⟨↑x, ⋯⟩, map_rel' := ⋯ } w.mapToSubgraph = SimpleGraph.Walk.induce s w hs

Mapping a walk to its own subgraph and then to G[s] where s contains the walk's support is the same as inducing the walk to s.

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Cited by

1 results in Mathlib

Foundations

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