isExtremal_free_iff — Mathlib

English

Extremal graphs with respect to H.Free are exactly H.Free graphs with edge count equal to extremalNumber(card V, H).

Русский

Экстремальные графы по $H.Free$ равны ровно $H.Free$ графы с количеством ребер равным экстремальному номеру.

LaTeX

$$\$ G.IsExtremal H.Free \\iff (H.Free G) \\land |G.edgeFinset| = \\mathrm{extremalNumber}(\\mathrm{card} V, H) \$$$

Lean4

/-- `H`-free extremal graphs are `H`-free simple graphs having `extremalNumber (card V) H` many
edges. -/
theorem isExtremal_free_iff : G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (card V) H :=
  by
  rw [IsExtremal, and_congr_right_iff, ← extremalNumber_le_iff]
  exact fun h ↦ ⟨eq_of_le_of_ge (card_edgeFinset_le_extremalNumber h), ge_of_eq⟩

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