Theorems · Theorem · combinatorics

SimpleGraph.triangle_removal

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 →
    ∃ G' ≤ G, ∃ x, ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3

Triangle Removal Lemma. If there are not too many triangles (on the order of (card α)^3) then they can all be removed by removing a few edges (on the order of (card α)^2).

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableRel