farFromTriangleFree_iff — Mathlib

English

G is ε-far from triangle-free iff for every subgraph H ≤ G with no triangles, the edge deficit is at least ε|α|^2.

Русский

G удалён на ε от треугольников тогда и только тогда, для каждого подграфа H ≤ G без треугольников, дефицит рёбер не менее ε|α|^2.

LaTeX

$$$G.\\text{FarFromTriangleFree } ε \\iff \\forall H,\\; [H\\le G]\\to H.\\text{CliqueFree }3 \\Rightarrow ε|\\alpha|^2 \\le |E(G)|-|E(H)|$$$

Lean4

theorem farFromTriangleFree_iff :
    G.FarFromTriangleFree ε ↔
      ∀ ⦃H : SimpleGraph α⦄,
        [DecidableRel H.Adj] → H ≤ G → H.CliqueFree 3 → ε * (card α ^ 2 : ℕ) ≤ #G.edgeFinset - #H.edgeFinset :=
  deleteFar_iff

Похожие утверждения