Erdős problem 23

The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

23.lean

Retained formal statement1 of 6

The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges.

FormalConjectures/ErdosProblems/23.leanErdos23.blowupC5_tight2 linesExact file

1∀ (n : ℕ),2  0 < n → ∀ H ≤ Erdos23.blowupC5 n, H.IsBipartite → n ^ 2 ≤ ((Erdos23.blowupC5 n).edgeFinset \ H.edgeFinset).card

TestStatement only, no proof