theorem ContinuousFunctions.intermediate_value_theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) : (∀ (y : ℝ), f a < y → y < f b → ∃ c ∈ Set.Ioo a b, f c = y) ∧ ∀ (y : ℝ), f b < y → y < f a → ∃ c ∈ Set.Ioo a b, f c = y

Bolzano's Intermediate Value Theorem.

Let f : ℝ → ℝ be continuous on [a, b] with a < b. Then:

• if f a < y < f b, there exists c ∈ (a, b) with f c = y;
• if f b < y < f a, there exists c ∈ (a, b) with f c = y.

In either case, f attains every value strictly between f a and f b at some interior point of the interval.

theorem ContinuousFunctions.polynomial_has_real_root : ∃ (x : ℝ), x ^ 2021 + x ^ 2020 + 9.03 * x + 1 = 0

The polynomial f(x) = x^2021 + x^2020 + 9.03 x + 1 has at least one real root.

Proved via the Intermediate Value Theorem: f(-1) < 0 and f(0) > 0, so by continuity there exists c ∈ [-1, 0] with f(c) = 0.