Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.farFromTriangleFree

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] (t : Finset (α × β × γ)) [inst_3 : DecidableEq α] [inst_4 : DecidableEq β]
  [inst_5 : DecidableEq γ] [inst_6 : Fintype α] [inst_7 : Fintype β] [inst_8 : Fintype γ]
  [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] {ε : 𝕜},
  ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑t.card →
    (SimpleGraph.TripartiteFromTriangles.graph t).FarFromTriangleFree ε

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingDecidableEqDecidableEqDecidableEqFintypeFintypeFintypeSimpleGraph.TripartiteFromTriangles.ExplicitDisjoint