Commit 2026-08-16 09:33 062f1e3d

View on Github →

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

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.IsCircuit.cycleBypass_eq_self_iff_isCycle

added theorem SimpleGraph.Walk.IsCircuit.length_cycleBypass_lt_iff_not_isCycle

added theorem SimpleGraph.Walk.IsCycle.cycleBypass_eq_self

added theorem SimpleGraph.Walk.IsTrail.cycleBypass_eq_self_iff_isCycle_or_nil

added theorem SimpleGraph.Walk.IsTrail.length_cycleBypass_lt_iff_not_isCycle_and_not_nil

added theorem SimpleGraph.Walk.bypass_cons_nil

added theorem SimpleGraph.Walk.bypass_eq_self_iff_isPath

deleted theorem SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass

added theorem SimpleGraph.Walk.cycleBypass_eq_self_iff_length_le

added theorem SimpleGraph.Walk.length_le_bypass_length_iff

added theorem SimpleGraph.Walk.nil_bypass