intermediate_value_univ — Mathlib

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

Похожие утверждения