English
Let G be a simple graph on a finite vertex set V. For a fixed natural number r, G is r-Turán-maximal if G contains no (r+1)-clique and, among all (r+1)-clique-free graphs on the same vertex set, G has the greatest possible number of edges (i.e., no other (r+1)-clique-free graph on V has more edges).
Русский
Пусть G — простой граф на конечном наборе вершин V. Пусть для фиксированного r граф G является r-турэновской максимальностью, если в G отсутствуют клики размера r+1, и среди всех графов на тех же вершинах, не содержащих клики размера r+1, G имеет наибольшее возможное число ребер (то есть для любого другого графа H на V с cliqueFree(r+1) верно |E(H)| ≤ |E(G)|).
LaTeX
$$$G \text{ is Turán-maximal for } r \iff G \text{ is } (r+1)\text{-clique-free} \land \forall H\,(H \text{ is } (r+1)\text{-clique-free} \rightarrow |E(H)| \le |E(G)|).$$$
Lean4
/-- An `r + 1`-cliquefree graph is `r`-Turán-maximal if any other `r + 1`-cliquefree graph on
the same vertex set has the same or fewer number of edges. -/
def IsTuranMaximal (r : ℕ) : Prop :=
G.CliqueFree (r + 1) ∧
∀ (H : SimpleGraph V) [DecidableRel H.Adj], H.CliqueFree (r + 1) → #H.edgeFinset ≤ #G.edgeFinset
