card_edgeFinset_of_isExtremal_free

English

If G is extremal with respect to H.Free, then the number of edges of G equals the extremal number.

Русский

Если $G$ экстремален по отношению к $H.Free$, то число ребер графа $G$ равно экстремальному номеру.

LaTeX

$$(isExtremal_free_iff.mp h).2$$

Lean4

theorem card_edgeFinset_of_isExtremal_free (h : G.IsExtremal H.Free) : #G.edgeFinset = extremalNumber (card V) H :=
  (isExtremal_free_iff.mp h).2

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