English
If a graph is ε-far from triangle-free, then ε is strictly smaller than one half.
Русский
Если граф далек от треугольников по ε, то ε меньше половины.
LaTeX
$$$\\varepsilon < 2^{-1}$$$
Lean4
theorem card_edgeFinset (hG : G.LocallyLinear) : #G.edgeFinset = 3 * #(G.cliqueFinset 3) :=
by
refine hG.edgeDisjointTriangles.card_edgeFinset_le.antisymm' ?_
rw [← mul_comm, ← mul_one #_]
refine card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_
· simpa [Sym2.forall, Nat.one_le_iff_ne_zero, -Finset.card_eq_zero, Finset.card_ne_zero, Finset.Nonempty] using hG.2
simp only [mem_cliqueFinset_iff, is3Clique_iff, forall_exists_index, and_imp]
rintro _ a b c hab hac hbc rfl
calc
_ ≤ #{s(a, b), s(a, c), s(b, c)} := card_le_card ?_
_ ≤ 3 := (card_insert_le _ _).trans (succ_le_succ <| (card_insert_le _ _).trans_eq <| by rw [card_singleton])
simp only [subset_iff, Sym2.forall, mem_sym2_iff, mem_bipartiteBelow, mem_insert, mem_edgeFinset, mem_singleton,
and_imp, mem_edgeSet, Sym2.mem_iff, forall_eq_or_imp, forall_eq]
rintro d e hde (rfl | rfl | rfl) (rfl | rfl | rfl) <;> simp [*] at *
