Commit 2025-03-08 05:25 59c6f604

View on Github →

feat(Combinatorics/SimpleGraph): API for bipartite simple graph double-counting (#20838) Implement an API for bipartite double-counting arguments using simple graph definitions. Notably define the predicate IsBipartite: G.IsBipartite s t is the proposition that G is bipartite in sets s, t.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Enumerative/DoubleCounting.lean

Created Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

added theorem SimpleGraph.IsBipartiteWith.mem_of_mem_adj'

added theorem SimpleGraph.IsBipartiteWith.mem_of_mem_adj

added theorem SimpleGraph.IsBipartiteWith.symm

added structure SimpleGraph.IsBipartiteWith

added theorem SimpleGraph.isBipartiteWith_bipartiteAbove

added theorem SimpleGraph.isBipartiteWith_bipartiteBelow

added theorem SimpleGraph.isBipartiteWith_comm

added theorem SimpleGraph.isBipartiteWith_degree_le'

added theorem SimpleGraph.isBipartiteWith_degree_le

added theorem SimpleGraph.isBipartiteWith_neighborFinset'

added theorem SimpleGraph.isBipartiteWith_neighborFinset

added theorem SimpleGraph.isBipartiteWith_neighborFinset_disjoint'

added theorem SimpleGraph.isBipartiteWith_neighborFinset_disjoint

added theorem SimpleGraph.isBipartiteWith_neighborFinset_subset'

added theorem SimpleGraph.isBipartiteWith_neighborFinset_subset

added theorem SimpleGraph.isBipartiteWith_neighborSet'

added theorem SimpleGraph.isBipartiteWith_neighborSet

added theorem SimpleGraph.isBipartiteWith_neighborSet_disjoint'

added theorem SimpleGraph.isBipartiteWith_neighborSet_disjoint

added theorem SimpleGraph.isBipartiteWith_neighborSet_subset'

added theorem SimpleGraph.isBipartiteWith_neighborSet_subset

added theorem SimpleGraph.isBipartiteWith_sum_degrees_eq

added theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges'

added theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges

added theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges

added theorem SimpleGraph.isBipartiteWith_support_subset

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

added theorem SimpleGraph.sum_degrees_support_eq_twice_card_edges

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.degree_eq_zero_iff_not_mem_support

added theorem SimpleGraph.degree_pos_iff_mem_support