Theorems · Theorem · combinatorics

SimpleGraph.Walk.exists_boundary_dart

∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V),
  u ∈ S → v ∉ S → ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Given a set S and a walk w from u to v such that u ∈ S but v ∉ S, there exists a dart in the walk whose start is in S but whose end is not.

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Cited by

3 results in Mathlib

Foundations

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