Theorems · Theorem · combinatorics

SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  G.FarFromTriangleFree ε → SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card

Triangle Removal Lemma. If not all triangles can be removed by removing few edges (on the order of (card α)^2), then there were many triangles to start with (on the order of (card α)^3).

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableRel