Bipartite graphs

This file proves results about bipartite simple graphs, including several double-counting arguments.

Main definitions

• SimpleGraph.IsBipartiteWith G s t is the condition that a simple graph G is bipartite in sets s, t, that is, s and t are disjoint and vertices v, w being adjacent in G implies that v ∈ s and w ∈ t, or v ∈ s and w ∈ t.

  Note that in this implementation, if G.IsBipartiteWith s t, s ∪ t need not cover the vertices of G, instead s ∪ t is only required to cover the support of G, that is, the vertices that form edges in G. This definition is equivalent to the expected definition. If s and t do not cover all the vertices, one recovers a covering of all the vertices by unioning the missing vertices (s ∪ t)ᶜ to either s or t.

• SimpleGraph.isBipartiteWith_sum_degrees_eq is the proof that if G.IsBipartiteWith s t, then the sum of the degrees of the vertices in s is equal to the sum of the degrees of the vertices in t.

• SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges is the proof that if G.IsBipartiteWith s t, then sum of the degrees of the vertices in s is equal to the number of edges in G.

  See SimpleGraph.sum_degrees_eq_twice_card_edges for the general version, and SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges' for the version from the "right".

Implementation notes

For the formulation of double-counting arguments where a bipartite graph is considered as a relation r : α → β → Prop, see Mathlib.Combinatorics.Enumerative.DoubleCounting.

TODO

• Define G.IsBipartite := G.Colorable 2 and prove G.IsBipartite iff there exist sets s t : Set V such that G.IsBipartiteWith s t.

• Prove that G.IsBipartite iff G does not contain an odd cycle. I.e., G.IsBipartite ↔ ∀ n, (cycleGraph (2*n+1)).Free G.

structure SimpleGraph.IsBipartiteWith {V : Type u_1} (G : SimpleGraph V) (s t : Set V) : Prop

G is bipartite in sets s and t iff s and t are disjoint and if vertices v and w are adjacent in G then v ∈ s and w ∈ t, or v ∈ t and w ∈ s.

• disjoint : Disjoint s t
• mem_of_adj ⦃v w : V⦄ : G.Adj v w → v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s

theorem SimpleGraph.IsBipartiteWith.symm {V : Type u_1} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) : G.IsBipartiteWith t s

theorem SimpleGraph.isBipartiteWith_comm {V : Type u_1} {G : SimpleGraph V} {s t : Set V} : G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s

theorem SimpleGraph.IsBipartiteWith.mem_of_mem_adj {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hv : v ∈ s) (hadj : G.Adj v w) : w ∈ t

If G.IsBipartiteWith s t and v ∈ s, then if v is adjacent to w in G then w ∈ t.

theorem SimpleGraph.isBipartiteWith_neighborSet {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G.neighborSet v = {w : V | w ∈ t ∧ G.Adj v w}

If G.IsBipartiteWith s t and v ∈ s, then the neighbor set of v is the set of vertices in t adjacent to v in G.

theorem SimpleGraph.isBipartiteWith_neighborSet_subset {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G.neighborSet v ⊆ t

If G.IsBipartiteWith s t and v ∈ s, then the neighbor set of v is a subset of t.

theorem SimpleGraph.isBipartiteWith_neighborSet_disjoint {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hv : v ∈ s) : Disjoint (G.neighborSet v) s

If G.IsBipartiteWith s t and v ∈ s, then the neighbor set of v is disjoint to s.

theorem SimpleGraph.IsBipartiteWith.mem_of_mem_adj' {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hw : w ∈ t) (hadj : G.Adj v w) : v ∈ s

If G.IsBipartiteWith s t and w ∈ t, then if v is adjacent to w in G then v ∈ s.

theorem SimpleGraph.isBipartiteWith_neighborSet' {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.neighborSet w = {v : V | v ∈ s ∧ G.Adj v w}

If G.IsBipartiteWith s t and w ∈ t, then the neighbor set of w is the set of vertices in s adjacent to w in G.

theorem SimpleGraph.isBipartiteWith_neighborSet_subset' {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.neighborSet w ⊆ s

If G.IsBipartiteWith s t and w ∈ t, then the neighbor set of w is a subset of s.

theorem SimpleGraph.isBipartiteWith_support_subset {V : Type u_1} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) : G.support ⊆ s ∪ t

If G.IsBipartiteWith s t, then the support of G is a subset of s ∪ t.

theorem SimpleGraph.isBipartiteWith_neighborSet_disjoint' {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (hw : w ∈ t) : Disjoint (G.neighborSet w) t

If G.IsBipartiteWith s t and w ∈ t, then the neighbor set of w is disjoint to t.

theorem SimpleGraph.isBipartiteWith_neighborFinset {V : Type u_1} {v : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hv : v ∈ s) : G.neighborFinset v = {w ∈ t | G.Adj v w}

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is the set of vertices in s adjacent to v in G.

theorem SimpleGraph.isBipartiteWith_bipartiteAbove {V : Type u_1} {v : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hv : v ∈ s) : G.neighborFinset v = Finset.bipartiteAbove G.Adj t v

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is the set of vertices "above" v according to the adjacency relation of G.

theorem SimpleGraph.isBipartiteWith_neighborFinset_subset {V : Type u_1} {v : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hv : v ∈ s) : G.neighborFinset v ⊆ t

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is a subset of s.

theorem SimpleGraph.isBipartiteWith_neighborFinset_disjoint {V : Type u_1} {v : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hv : v ∈ s) : Disjoint (G.neighborFinset v) s

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is disjoint to s.

theorem SimpleGraph.isBipartiteWith_degree_le {V : Type u_1} {v : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hv : v ∈ s) : G.degree v ≤ t.card

If G.IsBipartiteWith s t and v ∈ s, then the degree of v in G is at most the size of t.

theorem SimpleGraph.isBipartiteWith_neighborFinset' {V : Type u_1} {w : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hw : w ∈ t) : G.neighborFinset w = {v ∈ s | G.Adj v w}

If G.IsBipartiteWith s t and w ∈ t, then the neighbor finset of w is the set of vertices in s adjacent to w in G.

theorem SimpleGraph.isBipartiteWith_bipartiteBelow {V : Type u_1} {w : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hw : w ∈ t) : G.neighborFinset w = Finset.bipartiteBelow G.Adj s w

If G.IsBipartiteWith s t and w ∈ t, then the neighbor finset of w is the set of vertices "below" w according to the adjacency relation of G.

theorem SimpleGraph.isBipartiteWith_neighborFinset_subset' {V : Type u_1} {w : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hw : w ∈ t) : G.neighborFinset w ⊆ s

If G.IsBipartiteWith s t and w ∈ t, then the neighbor finset of w is a subset of s.

theorem SimpleGraph.isBipartiteWith_neighborFinset_disjoint' {V : Type u_1} {w : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hw : w ∈ t) : Disjoint (G.neighborFinset w) t

If G.IsBipartiteWith s t and w ∈ t, then the neighbor finset of w is disjoint to t.

theorem SimpleGraph.isBipartiteWith_degree_le' {V : Type u_1} {w : V} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) (hw : w ∈ t) : G.degree w ≤ s.card

If G.IsBipartiteWith s t and w ∈ t, then the degree of w in G is at most the size of s.

theorem SimpleGraph.isBipartiteWith_sum_degrees_eq {V : Type u_1} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) : ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w

If G.IsBipartiteWith s t, then the sum of the degrees of vertices in s is equal to the sum of the degrees of vertices in t.

See Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow.

theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges {V : Type u_1} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] [DecidableEq V] (h : G.IsBipartiteWith ↑s ↑t) : ∑ v ∈ s ∪ t, G.degree v = 2 * G.edgeFinset.card

theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges {V : Type u_1} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] [DecidableEq V] (h : G.IsBipartiteWith ↑s ↑t) : ∑ v ∈ s, G.degree v = G.edgeFinset.card

The degree-sum formula for bipartite graphs, summing over the "left" part.

See SimpleGraph.sum_degrees_eq_twice_card_edges for the general version, and SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges' for the version from the "right".

theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges' {V : Type u_1} {G : SimpleGraph V} [Fintype V] {s t : Finset V} [DecidableRel G.Adj] [DecidableEq V] (h : G.IsBipartiteWith ↑s ↑t) : ∑ v ∈ t, G.degree v = G.edgeFinset.card

The degree-sum formula for bipartite graphs, summing over the "right" part.

See SimpleGraph.sum_degrees_eq_twice_card_edges for the general version, and SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges for the version from the "left".