Commit 2025-02-21 11:42 012675bf

View on Github →

chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) Since Walk is becoming a long file, and with #21250 would be pushed over the limit, this PR extracts the WalkDecomp section, along with one lemma that depends on it to a seperate file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

added theorem SimpleGraph.Walk.count_edges_takeUntil_le_one

added theorem SimpleGraph.Walk.count_support_takeUntil_eq_one

added theorem SimpleGraph.Walk.darts_dropUntil_subset

added theorem SimpleGraph.Walk.darts_takeUntil_subset

added def SimpleGraph.Walk.dropUntil

added theorem SimpleGraph.Walk.dropUntil_copy

added theorem SimpleGraph.Walk.edges_dropUntil_subset

added theorem SimpleGraph.Walk.edges_takeUntil_subset

added theorem SimpleGraph.Walk.length_dropUntil_le

added theorem SimpleGraph.Walk.length_takeUntil_le

added theorem SimpleGraph.Walk.mem_support_iff_exists_append

added theorem SimpleGraph.Walk.mem_support_iff_exists_getVert

added def SimpleGraph.Walk.rotate

added theorem SimpleGraph.Walk.rotate_darts

added theorem SimpleGraph.Walk.rotate_edges

added theorem SimpleGraph.Walk.support_dropUntil_subset

added theorem SimpleGraph.Walk.support_rotate

added theorem SimpleGraph.Walk.support_takeUntil_subset

added def SimpleGraph.Walk.takeUntil

added theorem SimpleGraph.Walk.takeUntil_copy

added theorem SimpleGraph.Walk.take_spec

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

deleted theorem SimpleGraph.Walk.count_edges_takeUntil_le_one

deleted theorem SimpleGraph.Walk.count_support_takeUntil_eq_one

deleted theorem SimpleGraph.Walk.darts_dropUntil_subset

deleted theorem SimpleGraph.Walk.darts_takeUntil_subset

deleted def SimpleGraph.Walk.dropUntil

deleted theorem SimpleGraph.Walk.dropUntil_copy

deleted theorem SimpleGraph.Walk.edges_dropUntil_subset

deleted theorem SimpleGraph.Walk.edges_takeUntil_subset

deleted theorem SimpleGraph.Walk.length_dropUntil_le

deleted theorem SimpleGraph.Walk.length_takeUntil_le

deleted theorem SimpleGraph.Walk.mem_support_iff_exists_append

deleted theorem SimpleGraph.Walk.mem_support_iff_exists_getVert

deleted def SimpleGraph.Walk.rotate

deleted theorem SimpleGraph.Walk.rotate_darts

deleted theorem SimpleGraph.Walk.rotate_edges

deleted theorem SimpleGraph.Walk.support_dropUntil_subset

deleted theorem SimpleGraph.Walk.support_rotate

deleted theorem SimpleGraph.Walk.support_takeUntil_subset

deleted def SimpleGraph.Walk.takeUntil

deleted theorem SimpleGraph.Walk.takeUntil_copy

deleted theorem SimpleGraph.Walk.take_spec