of_extremalNumber_lt_card_edgeFinset

English

If graphs are isomorphic with the same vertex count, their extremal numbers are equal.

Русский

Если графы изоморфны и имеют одинаковое число вершин, их экстремальные номера равны.

LaTeX

$$\$\\forall n, H_1 \\cong_g H_2 \\Rightarrow \\mathrm{extremalNumber}(n,H_1)=\\mathrm{extremalNumber}(n,H_2)\$$$

Lean4

/-- If `G` has more than `extremalNumber (card V) H` edges, then `G` contains a copy of `H`. -/
theorem of_extremalNumber_lt_card_edgeFinset (h : extremalNumber (card V) H < #G.edgeFinset) : H ⊑ G :=
  by
  contrapose h; push_neg
  exact card_edgeFinset_le_extremalNumber h

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