theorem ContainersTriangleFree.containers_triangle_free (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ∃ (𝒞 : Finset (SimpleGraph (Fin n))), ↑𝒞.card ≤ ↑n ^ (C * ↑n ^ (3 / 2)) ∧ (∀ G ∈ 𝒞, ↑G.edgeFinset.card ≤ (1 / 4 + ε) * ↑n ^ 2) ∧ ∀ (H : SimpleGraph (Fin n)), H.CliqueFree 3 → ∃ G ∈ 𝒞, H ≤ G

Theorem 11.1.1 (Containers for triangle-free graphs). For every $\varepsilon > 0$, there is a constant $C > 0$ such that for every $n$ there is a family $\mathcal{C}$ of graphs on $[n]$ with:

• $|\mathcal{C}| \leq n^{C n^{3/2}}$;
• every $G \in \mathcal{C}$ has at most $(1/4 + \varepsilon) n^2$ edges;
• every triangle-free graph on $[n]$ is contained in some $G \in \mathcal{C}$.