farFromTriangleFree — Mathlib

English

If t is explicitly disjoint and a size constraint holds, then the graph t is far from being triangle-free.

Русский

Если t имеет явную несоприкосновенность и выполняется размерное ограничение, то граф t далек от треугольников без кликов.

LaTeX

$$$ (graph\ t).FarFromTriangleFree\ \varepsilon$ under the given bounds$$

Lean4

theorem farFromTriangleFree [ExplicitDisjoint t] {ε : 𝕜}
    (ht : ε * ((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2 : ℕ) ≤ #t) : (graph t).FarFromTriangleFree ε :=
  farFromTriangleFree_of_disjoint_triangles (t.map toTriangle)
      (map_subset_iff_subset_preimage.2 fun x hx ↦ by simpa using toTriangle_is3Clique hx)
      (map_toTriangle_disjoint t) <|
    by simpa [add_assoc] using ht

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