Theorems · Inductive type · combinatorics

SimpleGraph.IsPathGraph3Compl

{α : Type u} → SimpleGraph α → α → α → α → 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.

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

12 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms