Commit 2024-07-04 06:52 dff9f5d7

View on Github →

feat(Combinatorics/SimpleGraph): interactions between ConnectedComponent and matchings (#11667) These are some supporting lemma's on the way to a proof of Tutte's theorem

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj

added def SimpleGraph.ConnectedComponent.recOn

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching

added theorem SimpleGraph.ConnectedComponent.odd_matches_node_outside

modified theorem SimpleGraph.Subgraph.IsMatching.even_card

added theorem SimpleGraph.Subgraph.IsMatching.induce_connectedComponent

modified theorem SimpleGraph.Subgraph.IsMatching.support_eq_verts

modified theorem SimpleGraph.Subgraph.IsMatching.toEdge.surjective

modified theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj

modified theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_toEdge_of_adj

modified def SimpleGraph.Subgraph.IsMatching

modified theorem SimpleGraph.Subgraph.IsPerfectMatching.even_card

added theorem SimpleGraph.Subgraph.IsPerfectMatching.induce_connectedComponent_isMatching

modified def SimpleGraph.Subgraph.IsPerfectMatching

modified theorem SimpleGraph.Subgraph.isMatching_iff_forall_degree

modified theorem SimpleGraph.Subgraph.isPerfectMatching_iff_forall_degree

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean