extremalNumber_le_iff — Mathlib

English

extremalNumber ≤ m is equivalent to saying every H-free graph has at most m edges.

Русский

extremalNumber ≤ m эквивалентно тому, что каждый граф без $H$ имеет не более $m$ ребер.

LaTeX

$$\$ extremalNumber(|V|) H ≤ m \\iff \\forall G, H.Free G \\Rightarrow |G.edgeFinset| ≤ m \$$$

Lean4

/-- `extremalNumber (card V) H` is at most `x` if and only if every `H`-free simple graph `G` has
at most `x` edges. -/
theorem extremalNumber_le_iff (H : SimpleGraph W) (m : ℕ) :
    extremalNumber (card V) H ≤ m ↔ ∀ ⦃G : SimpleGraph V⦄ [DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m :=
  by
  simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.sup_le_iff, mem_filter_univ]
  exact ⟨fun h _ _ h' ↦ by convert h _ h', fun h _ h' ↦ by convert h h'⟩

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