Complete Multipartite Graphs

A graph is complete multipartite iff non-adjacency is transitive.

Main declarations

• SimpleGraph.IsCompleteMultipartite: predicate for a graph to be complete-multi-partite.

• SimpleGraph.IsCompleteMultipartite.setoid: the Setoid given by non-adjacency.

• SimpleGraph.IsCompleteMultipartite.iso: the graph isomorphism from a graph that IsCompleteMultipartite to the corresponding completeMultipartiteGraph.

• SimpleGraph.IsPathGraph3Compl: predicate for three vertices to be a witness to non-complete-multi-partite-ness of a graph G. (The name refers to the fact that the three vertices form the complement of pathGraph 3.)

• See also: Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree a maximally r + 1- cliquefree graph is r-colorable iff it is complete-multipartite.

def SimpleGraph.IsCompleteMultipartite {α : Type u} (G : SimpleGraph α) : Prop

G is IsCompleteMultipartite iff non-adjacency is transitive

Equations

• G.IsCompleteMultipartite = Transitive fun (x1 x2 : α) => ¬G.Adj x1 x2

def SimpleGraph.IsCompleteMultipartite.setoid {α : Type u} {G : SimpleGraph α} (h : G.IsCompleteMultipartite) : Setoid α

The setoid given by non-adjacency

Equations

• h.setoid = { r := fun (x1 x2 : α) => ¬G.Adj x1 x2, iseqv := ⋯ }

theorem SimpleGraph.completeMultipartiteGraph.isCompleteMultipartite {ι : Type u_1} (V : ι → Type u_2) : (completeMultipartiteGraph V).IsCompleteMultipartite

def SimpleGraph.IsCompleteMultipartite.iso {α : Type u} {G : SimpleGraph α} (h : G.IsCompleteMultipartite) : G ≃g completeMultipartiteGraph fun (c : Quotient h.setoid) => { x : α // h.setoid c.out x }

The graph isomorphism from a graph G that IsCompleteMultipartite to the corresponding completeMultipartiteGraph (see also isCompleteMultipartite_iff)

Equations

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

theorem SimpleGraph.isCompleteMultipartite_iff {α : Type u} {G : SimpleGraph α} : G.IsCompleteMultipartite ↔ ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

theorem SimpleGraph.IsCompleteMultipartite.colorable_of_cliqueFree {α : Type u} {G : SimpleGraph α} {n : ℕ} (h : G.IsCompleteMultipartite) (hc : G.CliqueFree n) : G.Colorable (n - 1)

structure SimpleGraph.IsPathGraph3Compl {α : Type u} (G : SimpleGraph α) (v w₁ w₂ : α) : Prop

The vertices v, w₁, w₂ form an IsPathGraph3Compl in G iff w₁w₂ is the only edge present between these three vertices. It is a witness to the non-complete-multipartite-ness of G (see not_isCompleteMultipartite_iff_exists_isPathGraph3Compl). This structure is an explicit way of saying that the induced graph on {v, w₁, w₂} is the complement of P3.

• adj : G.Adj w₁ w₂
• not_adj_fst : ¬G.Adj v w₁
• not_adj_snd : ¬G.Adj v w₂

theorem SimpleGraph.IsPathGraph3Compl.ne_fst {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : v ≠ w₁

theorem SimpleGraph.IsPathGraph3Compl.ne_snd {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : v ≠ w₂

theorem SimpleGraph.IsPathGraph3Compl.fst_ne_snd {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : w₁ ≠ w₂

theorem SimpleGraph.IsPathGraph3Compl.symm {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) : G.IsPathGraph3Compl v w₂ w₁

theorem SimpleGraph.exists_isPathGraph3Compl_of_not_isCompleteMultipartite {α : Type u} {G : SimpleGraph α} (h : ¬G.IsCompleteMultipartite) : ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

theorem SimpleGraph.not_isCompleteMultipartite_iff_exists_isPathGraph3Compl {α : Type u} {G : SimpleGraph α} : ¬G.IsCompleteMultipartite ↔ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

def SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) : (pathGraph 3)ᶜ ↪g G

Any IsPathGraph3Compl in G gives rise to a graph embedding of the complement of the path graph

Equations

• h.pathGraph3ComplEmbedding = { toFun := fun (x : Fin 3) => match x with | 0 => w₁ | 1 => v | 2 => w₂, inj' := ⋯, map_rel_iff' := ⋯ }

noncomputable def SimpleGraph.pathGraph3ComplEmbeddingOf {α : Type u} {G : SimpleGraph α} (h : ¬G.IsCompleteMultipartite) : (pathGraph 3)ᶜ ↪g G

Embedding of (pathGraph 3)ᶜ into G that is not complete-multipartite.

Equations

• SimpleGraph.pathGraph3ComplEmbeddingOf h = ⋯.pathGraph3ComplEmbedding

theorem SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding {α : Type u} {G : SimpleGraph α} (e : (pathGraph 3)ᶜ ↪g G) : ¬G.IsCompleteMultipartite

theorem SimpleGraph.IsCompleteMultipartite.comap {α : Type u} {G : SimpleGraph α} {β : Type u_1} {H : SimpleGraph β} (f : H ↪g G) : G.IsCompleteMultipartite → H.IsCompleteMultipartite