Theorems · Inductive type · combinatorics

SimpleGraph.IsFiveWheelLike

{α : Type u_1} → [DecidableEq α] → SimpleGraph α → ℕ → ℕ → α → α → α → Finset α → Finset α → Prop

An IsFiveWheelLike r k v w₁ w₂ s t structure in G consists of vertices v w₁ w₂ and r-sets s and t such that {v, w₁, w₂} induces the single edge w₁w₂ (i.e. they form an IsPathGraph3Compl), v, w₁, w₂ ∉ s ∪ t, s ∪ {v}, t ∪ {v}, s ∪ {w₁}, t ∪ {w₂} are all (r + 1)-cliques and #(s ∩ t) = k. (If G is maximally (r + 2)-cliquefree and not complete multipartite then G will contain such a structure: see exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite.)

Defined in

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Cited by

25 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

DecidableEq