card_edgeFinset_le_extremalNumber

English

If H.Free G, then the number of edges of G is bounded above by extremalNumber(card V, H).

Русский

Если $H.Free G$, то число ребер графа $G$ не превосходит \$\\mathrm{extremalNumber}(\\mathrm{card} V, H)\$.

LaTeX

$$\$ H.Free G \\Rightarrow |G.edgeFinset| \\le \\mathrm{extremalNumber}(\\mathrm{card} V, H) \$$$

Lean4

/-- If `G` is `H`-free, then `G` has at most `extremalNumber (card V) H` edges. -/
theorem card_edgeFinset_le_extremalNumber (h : H.Free G) : #G.edgeFinset ≤ extremalNumber (card V) H :=
  by
  rw [extremalNumber_of_fintypeCard_eq rfl]
  convert @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G (by simpa using h)

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