Theorem SimpleGraph.Walk.length_le_bypass_length_iff

Modification history

2026-08-16 09:33

Mathlib/Combinatorics/SimpleGraph/Paths.lean

feat(Combinatorics/SimpleGraph): add several lemmas about when `Walk.bypass` and `Walk.cycleBypass` do nothing (#37562)

Added SimpleGraph.Walk.length_le_bypass_length_iff View on Github →