le_iff_eq — Mathlib

English

Let G be r-Turán maximal. If H is an (r+1)-clique-free graph on the same vertex set, then G is contained in H (edge-wise) if and only if G = H. In particular, among all (r+1)-clique-free graphs on V, G is maximal in the subgraph order only when G = H.

Русский

Пусть G является r-турэновской максимальностью. Если H — граф на тех же вершинах, у которого отсутствуют клики размера r+1, то G содержится в H по ребрам тогда и только тогда G = H.

LaTeX

$$$G \text{ IsTuranMaximal } r \rightarrow H \text{ CliqueFree } (r+1) \rightarrow (G \le H \iff G = H).$$$

Lean4

theorem le_iff_eq (hG : G.IsTuranMaximal r) (hH : H.CliqueFree (r + 1)) : G ≤ H ↔ G = H := by
  classical
    exact
    ⟨fun hGH ↦ edgeFinset_inj.1 <| eq_of_subset_of_card_le (edgeFinset_subset_edgeFinset.2 hGH) (hG.2 _ hH), le_of_eq⟩

Похожие утверждения