Commit 2025-01-28 16:01 cefd4055

View on Github →

feat(Combinatorics/SimpleGraph/Matching): Interactions between spanningCoe, IsAlternating and IsCycles (#20800) Add basic results in preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.IsAlternating.mono

added theorem SimpleGraph.IsCycles.induce_supp

added theorem SimpleGraph.IsPerfectMatching.isAlternating_symmDiff_left

added theorem SimpleGraph.IsPerfectMatching.isAlternating_symmDiff_right

added theorem SimpleGraph.IsPerfectMatching.symmDiff_of_isAlternating

deleted theorem SimpleGraph.IsPerfectMatching.symmDiff_spanningCoe_of_isAlternating

added theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_isCycles

deleted theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_spanningCoe_IsCycles

added theorem SimpleGraph.Subgraph.IsPerfectMatching.toSubgraph_iff

deleted theorem SimpleGraph.Subgraph.IsPerfectMatching.toSubgraph_spanningCoe_iff

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_induce_supp

added theorem SimpleGraph.ConnectedComponent.mem_supp_congr_adj