Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  (SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3 = ⇑SimpleGraph.TripartiteFromTriangles.toTriangle '' ↑t

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqDecidableEqSimpleGraph.TripartiteFromTriangles.NoAccidental