Erdős problem 1044
Let where for all . If is the maximum of the lengths of the boundaries of the connected components of then determine the infimum of .
Sources
FormalConjectures/ErdosProblems/
1044.lean
Retained formal statement
Let where for all . If is the maximum of the lengths of the boundaries of the connected components of then determine the infimum of .
A problem of Erdős, Herzog, and Piranian [EHP58].
This has been resolved by Tang, who proved that the infimum of over all such is .
IsGLB {L | ∃ f, Erdos1044.IsAdmissible f ∧ Erdos1044.maxBoundaryLength f = L} 2