True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2