farFromTriangleFree_of_disjoint_triangles

English

Equivalences of logical forms used in the subsingleton characterisation.

Русский

Эквивалентности формулировок, используемые в характеристике через Subsingleton.

LaTeX

$$Eq (∀ (a : α), Or (Eq a b) (q a) → p a) (And (p b) (∀ a, q a → p a))$$

Lean4

/-- If there are `ε * (card α)^2` disjoint triangles, then the graph is `ε`-far from being
triangle-free. -/
theorem farFromTriangleFree_of_disjoint_triangles (tris : Finset (Finset α)) (htris : tris ⊆ G.cliqueFinset 3)
    (pd : (tris : Set (Finset α)).Pairwise fun x y ↦ (x ∩ y : Set α).Subsingleton)
    (tris_big : ε * (card α ^ 2 : ℕ) ≤ #tris) : G.FarFromTriangleFree ε :=
  by
  rw [farFromTriangleFree_iff]
  intro H _ hG hH
  rw [← Nat.cast_sub (card_le_card <| edgeFinset_mono hG)]
  exact tris_big.trans (Nat.cast_le.2 <| farFromTriangleFree_of_disjoint_triangles_aux htris pd hG hH)

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