English
For any H, m < extremalNumber(card V) H iff there exists a graph G with H.Free G and m < |G.edgeFinset|.
Русский
Для любого \(H\) и \(m\) выполняется: \(m < \\mathrm{extremalNumber}(|V|,H)\\) тогда и только тогда существует граф \(G\) с \(H.Free G\) и \(m < |G.edgeFinset|\.
LaTeX
$$\\( m < \\mathrm{extremalNumber}(\\mathrm{card} V, H) \\iff \\exists G, \\exists \\_ : DecidableRel G.Adj, H.Free G \\land m < |G.edgeFinset| \\)$$
Lean4
/-- `extremalNumber (card V) H` is greater than `x` if and only if there exists a `H`-free simple
graph `G` with more than `x` edges. -/
theorem lt_extremalNumber_iff (H : SimpleGraph W) (m : ℕ) :
m < extremalNumber (card V) H ↔ ∃ G : SimpleGraph V, ∃ _ : DecidableRel G.Adj, H.Free G ∧ m < #G.edgeFinset :=
by
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.lt_sup_iff, mem_filter_univ]
exact ⟨fun ⟨_, h, h'⟩ ↦ ⟨_, _, h, h'⟩, fun ⟨_, _, h, h'⟩ ↦ ⟨_, h, by convert h'⟩⟩
