English
If V is finite with card V = n, then extremalNumber n H equals the supremum over all G on V with H.Free G of |G.edgeFinset|.
Русский
Если \(V\) конечно, \(|V|=n\), то \\( \\mathrm{extremalNumber}(n,H)=\\sup\\{ |G|_{edgeFinset} : G\\ text{ на }V, H.Free G\\} \\).
LaTeX
$$\\( \\mathrm{extremalNumber}(n,H) = \\sup_{G:\\ SimpleGraph\\ V \\;:\\; H.Free G} |G.edgeFinset|$$
Lean4
theorem extremalNumber_of_fintypeCard_eq [Fintype V] (hc : card V = n) :
extremalNumber n H = sup {G : SimpleGraph V | H.Free G} (#·.edgeFinset) :=
by
let e := Fintype.equivFinOfCardEq hc
rw [extremalNumber, le_antisymm_iff]
and_intros
on_goal 1 => replace e := e.symm
all_goals
rw [Finset.sup_le_iff]
intro G h
let G' := G.map e.toEmbedding
replace h' : G' ∈ univ.filter (H.Free ·) :=
by
rw [mem_filter, ← free_congr .refl (.map e G)]
simpa using h
rw [Iso.card_edgeFinset_eq (.map e G)]
convert @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G' h'
