Theorem SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass

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)

Deleted SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass View on Github →

2026-06-01 01:24

Mathlib/Combinatorics/SimpleGraph/Paths.lean

feat(Combinatorics/SimpleGraph/Walk): upgrade subset theorems to sublist/prefix/suffix (#37577) …

Added SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass View on Github →