English
The extremal number of a natural n and a simple graph H is the maximum number of edges in an H-free simple graph on n vertices; if H is contained in all graphs on n vertices, this is 0.
Русский
Экстремальный номер \n-\u003e максимальное число ребер в графе без \(H\) на \(n\) вершинах; если \(H\) содержится во всех графах на \(n\) вершинах, то это \(0\).
LaTeX
$$\\( \\mathrm{extremalNumber}(n,H) = \\sup \\{ |G|_edgeFinset : G\\text{ на } n\\text{ вершинах}, H.Free G\\} \\)$$
Lean4
/-- The extremal number of a natural number `n` and a simple graph `H` is the maximum number of
edges in a `H`-free simple graph on `n` vertices.
If `H` is contained in all simple graphs on `n` vertices, then this is `0`. -/
noncomputable def extremalNumber (n : ℕ) {W : Type*} (H : SimpleGraph W) : ℕ :=
sup {G : SimpleGraph (Fin n) | H.Free G} (#·.edgeFinset)
