Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.is3Clique_iff

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)},
  (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 s ↔
    ∃ x ∈ t, SimpleGraph.TripartiteFromTriangles.toTriangle x = s

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqDecidableEqSimpleGraph.TripartiteFromTriangles.NoAccidental