Let $f\in \mathbb{C}[x]$ be a monic polynomial with $m$ distinct roots, and let $c>0$ be a constant small enough such that $\{ z: \lvert f(z)\rvert\leq c\}$ has $m$ distinct connected components.

1(Erdos1047.componentsIn2        (Erdos1047.strictSublevelSet ((Polynomial.X ^ 2 + 1) * (Polynomial.X - Polynomial.C 2) ^ 2)3          (5 ^ (3 / 2) / 4))).ncard =4    3 ∧5  ∃6    t ∈7      Erdos1047.componentsIn8        (Erdos1047.strictSublevelSet ((Polynomial.X ^ 2 + 1) * (Polynomial.X - Polynomial.C 2) ^ 2) (5 ^ (3 / 2) / 4)),9    ¬Convex ℝ t