English
In a locally linear graph, the number of edges is at least three times the number of 3-cliques.
Русский
В локально линейном графе число рёбер не меньше тройки числа кликов размера 3.
LaTeX
$$$3 \\cdot |G.cliqueFinset 3| \\le |G.edgeFinset|$$$
Lean4
theorem card_edgeFinset_le (hG : G.EdgeDisjointTriangles) : 3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset :=
by
rw [mul_comm, ← mul_one #G.edgeFinset]
refine card_mul_le_card_mul (fun s e ↦ e ∈ s.sym2) ?_ (fun e he ↦ ?_)
· simp only [is3Clique_iff, mem_cliqueFinset_iff, mem_sym2_iff, forall_exists_index, and_imp]
rintro _ a b c hab hac hbc rfl
have : #{s(a, b), s(a, c), s(b, c)} = 3 := by
refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩ <;> simp [hab.ne, hac.ne, hbc.ne]
rw [← this]
refine card_mono ?_
simp [insert_subset, *]
·
simpa only [card_le_one, mem_bipartiteBelow, and_imp, Set.Subsingleton, Set.mem_setOf_eq, mem_cliqueFinset_iff,
mem_cliqueSet_iff] using hG.mem_sym2_subsingleton (G.not_isDiag_of_mem_edgeSet <| mem_edgeFinset.1 he)
