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

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.

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

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 = inferInstanceAs (DecidableRel fun (v w : V) => G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s))

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