Theorems · Definition · combinatorics

SimpleGraph.FarFromTriangleFree

{α : Type u_1} →
  {𝕜 : Type u_3} → [Field 𝕜] → [LinearOrder 𝕜] → (G : SimpleGraph α) → 𝕜 → [Fintype α] → [DecidableRel G.Adj] → Prop

A simple graph is `ε`-far from triangle-free if one must remove at least ε * (card α) ^ 2 edges to make it triangle-free.

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderFintypeDecidableRel