FarFromTriangleFree — Mathlib

English

If there are sufficiently many vertex-disjoint triangles whose vertex sets lie inside G, then G is ε-far from triangle-free.

Русский

Если существует достаточно много парной независимой совокупности треугольников, чьи вершины лежат внутри G, то G далеко от треугольников.

LaTeX

$$$\\text{tris} \\subseteq G.cliqueFinset 3$, параллельно: пары множеств треугольников несовпадают;\\tris\\; \\Rightarrow \\ G.\\text{FarFromTriangleFree } ε$$$

Lean4

/-- A simple graph is *`ε`-far from triangle-free* if one must remove at least
`ε * (card α) ^ 2` edges to make it triangle-free. -/
def FarFromTriangleFree : Prop :=
  G.DeleteFar (fun H ↦ H.CliqueFree 3) <| ε * (card α ^ 2 : ℕ)

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