Documentation

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Complete Multipartite Graphs #

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

Main declarations #

See also: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike #

colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree a maximally r + 1- cliquefree graph is r-colorable iff it is complete-multipartite.

G is IsCompleteMultipartite iff non-adjacency is transitive

Equations

The setoid given by non-adjacency

Equations

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)
structure SimpleGraph.IsPathGraph3Compl {α : Type u} (G : SimpleGraph α) (v w₁ w₂ : α) :

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₂
def SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) :

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

Equations

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

Equations