English
If a continuous function f:X→α on a connected (or preconnected) space X attains a value ≤ c at some point and a value ≥ c at some other point, then c lies in the range of f.
Русский
Если непрерывная функция f принимает значение ≤ c в одной точке и ≥ c в другой, то c лежит в образе f.
LaTeX
$$$\text{Continuous}(f) \to (\exists a\, f(a) \le c) \to (\exists b\, c \le f(b)) \Rightarrow c \in \mathrm{range}(f)$$$
Lean4
/-- **Intermediate Value Theorem** for continuous functions on connected spaces. -/
theorem intermediate_value_univ [PreconnectedSpace X] (a b : X) {f : X → α} (hf : Continuous f) :
Icc (f a) (f b) ⊆ range f := fun _ hx => intermediate_value_univ₂ hf continuous_const hx.1 hx.2