Commit 2025-11-16 07:52 34b4f60e

View on Github →

feat: removing leaves from a connected graph keeps it connected (#31103) ... using properties of 2-connected components. From the ProofBench workshop

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.Preconnected.induce_of_degree_eq_one

added theorem SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable

added theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable

added theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_subsingleton_neighborSet

added theorem SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges

added theorem SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil

Modified Mathlib/Data/List/Nodup.lean