Commit 2025-04-17 18:29 579c35b7

View on Github →

feat(Combinatorics/SimpleGraph): miscellaneous walk lemmas (#22242) Adds some miscellaneous lemmas on walks, in preparation for Tutte's theorem.

Estimated changes

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

added theorem SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq

added theorem SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty

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

added theorem SimpleGraph.Walk.not_mem_support_takeUntil_support_takeUntil_subset

deleted theorem SimpleGraph.Walk.not_mem_support_takeUntil_takeUntil

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

added theorem SimpleGraph.Walk.exists_adj_adj_not_adj_ne

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.ConnectedComponent.connected_induce_supp

added theorem SimpleGraph.ConnectedComponent.reachable_induce_supp

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.exists_length_eq_one_iff