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.IsBipartite: Predicate for a simple graph to be bipartite. G.IsBipartite is defined as an abbreviation for G.Colorable 2.

• SimpleGraph.isBipartite_iff_exists_isBipartiteWith is the proof that G.IsBipartite iff G.IsBipartiteWith s 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".

• SimpleGraph.completeBipartiteGraph_isContained_iff is the proof that simple graphs contain a copy of a completeBipartiteGraph α β iff there exists a "left" subset of card α vertices and a "right" subset of card β vertices such that every vertex in the "left" subset is adjacent to every vertex in the "right" subset.

• SimpleGraph.between; the simple graph G.between s t is the subgraph of G containing edges that connect a vertex in the set s to a vertex in the set t.

• SimpleGraph.bipartiteDoubleCover; the simple graph G.bipartiteDoubleCover has two vertices inl v and inr v for each vertex v in G such that inl v (inr v) is adjacent to inr w (inl w) iff v is adjacent to w in G.

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.lean.

TODO

• 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} {s t : Finset V} [Fintype ↑(G.neighborSet 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_neighborFinset' {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [Fintype ↑(G.neighborSet w)] [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_bipartiteAbove {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [Fintype ↑(G.neighborSet 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_bipartiteBelow {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [Fintype ↑(G.neighborSet w)] [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} {v : V} {G : SimpleGraph V} {s t : Finset V} [Fintype ↑(G.neighborSet v)] (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} {s t : Finset V} [Fintype ↑(G.neighborSet v)] (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} {s t : Finset V} [Fintype ↑(G.neighborSet v)] (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_subset' {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [Fintype ↑(G.neighborSet w)] (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} {s t : Finset V} [Fintype ↑(G.neighborSet w)] (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} {s t : Finset V} [Fintype ↑(G.neighborSet w)] (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} {s t : Finset V} [G.LocallyFinite] (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} {s t : Finset V} [Fintype 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} {s t : Finset V} [Fintype V] [DecidableRel G.Adj] (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} {s t : Finset V} [Fintype V] [DecidableRel G.Adj] (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".

@[reducible, inline]

abbrev SimpleGraph.IsBipartite {V : Type u_1} (G : SimpleGraph V) : Prop

The predicate for a simple graph to be bipartite.

Equations

• G.IsBipartite = G.Colorable 2

theorem SimpleGraph.IsBipartite.exists_isBipartiteWith {V : Type u_1} {G : SimpleGraph V} (h : G.IsBipartite) : ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t

If a simple graph G is bipartite, then there exist disjoint sets s and t such that all edges in G connect a vertex in s to a vertex in t.

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

If a simple graph G has a bipartition, then it is bipartite.

theorem SimpleGraph.isBipartite_iff_exists_isBipartiteWith {V : Type u_1} {G : SimpleGraph V} : G.IsBipartite ↔ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t

G.IsBipartite if and only if G.IsBipartiteWith s t.

noncomputable def SimpleGraph.Copy.completeBipartiteGraph {V : Type u_1} {G : SimpleGraph V} {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (left right : Finset V) (card_left : left.card = Fintype.card α) (card_right : right.card = Fintype.card β) (h : G.IsCompleteBetween ↑left ↑right) : (_root_.completeBipartiteGraph α β).Copy G

A "left" subset of card α vertices and a "right" subset of card β vertices such that every vertex in the "left" subset is adjacent to every vertex in the "right" subset gives rise to a copy of a complete bipartite graph.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.completeBipartiteGraph_isContained_iff {V : Type u_1} {G : SimpleGraph V} {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] : (completeBipartiteGraph α β).IsContained G ↔ ∃ (left : Finset V) (right : Finset V), left.card = Fintype.card α ∧ right.card = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Simple graphs contain a copy of a completeBipartiteGraph α β iff there exists a "left" subset of card α vertices and a "right" subset of card β vertices such that every vertex in the "left" subset is adjacent to every vertex in the "right" subset.

theorem SimpleGraph.IsBipartiteWith.subgraph {V : Type u_1} {G : SimpleGraph V} {s t : Set V} (h : G.IsBipartiteWith s t) (H : G.Subgraph) : H.coe.IsBipartiteWith {x : ↑H.verts | ↑x ∈ s} {x : ↑H.verts | ↑x ∈ t}

theorem SimpleGraph.IsBipartite.subgraph {V : Type u_1} {G : SimpleGraph V} (h : G.IsBipartite) (H : G.Subgraph) : H.coe.IsBipartite

def SimpleGraph.between {V : Type u_1} (s t : Set V) (G : SimpleGraph V) : SimpleGraph V

The subgraph of G containing edges that connect a vertex in the set s to a vertex in the set t.

Equations

• SimpleGraph.between s t G = { Adj := fun (v w : V) => G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s), symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.between_adj {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V} : (between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)

theorem SimpleGraph.between_le {V : Type u_1} {G : SimpleGraph V} {s t : Set V} : between s t G ≤ G

theorem SimpleGraph.between_comm {V : Type u_1} {G : SimpleGraph V} {s t : Set V} : between s t G = between t s G

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjBetweenOfDecidablePredMemSet {V : Type u_1} {G : SimpleGraph V} {s t : Set V} [DecidableRel G.Adj] [DecidablePred fun (x : V) => x ∈ s] [DecidablePred fun (x : V) => x ∈ t] : DecidableRel (between s t G).Adj

Equations

• SimpleGraph.instDecidableRelAdjBetweenOfDecidablePredMemSet = SimpleGraph.instDecidableRelAdjBetweenOfDecidablePredMemSet._aux_1

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

G.between s t is bipartite if the sets s and t are disjoint.

theorem SimpleGraph.between_isBipartite {V : Type u_1} {G : SimpleGraph V} {s t : Set V} (h : Disjoint s t) : (between s t G).IsBipartite

G.between s t is bipartite if the sets s and t are disjoint.

theorem SimpleGraph.neighborSet_subset_between_union {V : Type u_1} {v : V} {G : SimpleGraph V} {s : Set V} (hv : v ∈ s) : G.neighborSet v ⊆ (between s sᶜ G).neighborSet v ∪ s

The neighbor set of v ∈ s in G.between s sᶜ excludes the vertices in s adjacent to v in G.

theorem SimpleGraph.neighborSet_subset_between_union_compl {V : Type u_1} {w : V} {G : SimpleGraph V} {s : Set V} (hw : w ∈ sᶜ) : G.neighborSet w ⊆ (between s sᶜ G).neighborSet w ∪ sᶜ

The neighbor set of w ∈ sᶜ in G.between s sᶜ excludes the vertices in sᶜ adjacent to w in G.

theorem SimpleGraph.neighborFinset_subset_between_union {V : Type u_1} {v : V} {G : SimpleGraph V} [DecidableEq V] [Fintype V] {s : Finset V} [DecidableRel G.Adj] (hv : v ∈ s) : G.neighborFinset v ⊆ (between (↑s) (↑s)ᶜ G).neighborFinset v ∪ s

The neighbor finset of v ∈ s in G.between s sᶜ excludes the vertices in s adjacent to v in G.

theorem SimpleGraph.degree_le_between_add {V : Type u_1} {v : V} {G : SimpleGraph V} [DecidableEq V] [Fintype V] {s : Finset V} [DecidableRel G.Adj] (hv : v ∈ s) : G.degree v ≤ (between (↑s) (↑s)ᶜ G).degree v + s.card

The degree of v ∈ s in G is at most the degree in G.between s sᶜ plus the excluded vertices from s.

theorem SimpleGraph.neighborFinset_subset_between_union_compl {V : Type u_1} {w : V} {G : SimpleGraph V} [DecidableEq V] [Fintype V] {s : Finset V} [DecidableRel G.Adj] (hw : w ∈ sᶜ) : G.neighborFinset w ⊆ (between (↑s) (↑s)ᶜ G).neighborFinset w ∪ sᶜ

The neighbor finset of w ∈ sᶜ in G.between s sᶜ excludes the vertices in sᶜ adjacent to w in G.

theorem SimpleGraph.degree_le_between_add_compl {V : Type u_1} {w : V} {G : SimpleGraph V} [DecidableEq V] [Fintype V] {s : Finset V} [DecidableRel G.Adj] (hw : w ∈ sᶜ) : G.degree w ≤ (between (↑s) (↑s)ᶜ G).degree w + sᶜ.card

The degree of w ∈ sᶜ in G is at most the degree in G.between s sᶜ plus the excluded vertices from sᶜ.

def SimpleGraph.bipartiteDoubleCover {V : Type u_1} (G : SimpleGraph V) : SimpleGraph (V ⊕ V)

bipartiteDoubleCover G has two vertices inl v and inr v for each vertex v in G such that inl v (inr v) is adjacent to inr w (inl w) iff v is adjacent to w in G.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover {V : Type u_1} {G : SimpleGraph V} [h : DecidableRel G.Adj] : DecidableRel G.bipartiteDoubleCover.Adj

Equations

• SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover (Sum.inl val) (Sum.inr val_1) = h val val_1
• SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover (Sum.inr val) (Sum.inl val_1) = h val val_1
• SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover (Sum.inl val) (Sum.inl val_1) = isFalse ⋯
• SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover (Sum.inr val) (Sum.inr val_1) = isFalse ⋯

theorem SimpleGraph.bipartiteDoubleCover_le {V : Type u_1} {G : SimpleGraph V} : G.bipartiteDoubleCover ≤ completeBipartiteGraph V V

The bipartite double cover of G is contained in the corresponding complete bipartite graph, that is, the bipartite double cover of G is bipartite.

theorem SimpleGraph.card_edgeFinset_bipartiteDoubleCover {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] : G.bipartiteDoubleCover.edgeFinset.card = 2 * G.edgeFinset.card

The bipartite double cover of G has twice the number of edges as G.

theorem SimpleGraph.completeBipartiteGraph_isContained_bipartiteDoubleCover {V : Type u_1} {G : SimpleGraph V} {α : Type u_2} {β : Type u_3} [Finite α] [Finite β] [Nonempty α] [Nonempty β] : (completeBipartiteGraph α β).IsContained G.bipartiteDoubleCover ↔ (completeBipartiteGraph α β).IsContained G

If the double cover of G contains completeBipartiteGraph α β, then G also contains completeBipartiteGraph α β.

theorem SimpleGraph.isBipartiteWith_bipartiteDoubleCover {V : Type u_1} {G : SimpleGraph V} : G.bipartiteDoubleCover.IsBipartiteWith {v : V ⊕ V | v.isLeft = true} {w : V ⊕ V | w.isRight = true}

theorem SimpleGraph.isBipartite_bipartiteDoubleCover {V : Type u_1} {G : SimpleGraph V} : G.bipartiteDoubleCover.IsBipartite