intermediate_value_uIcc — Mathlib

English

If f is continuous on the closed interval Icc(a,b), then [min{f(a),f(b)}, max{f(a),f(b)}] ⊆ f([a,b]).

Русский

Если f непрерывна на замкнутом интервале Icc(a,b), то [min{f(a),f(b)}, max{f(a),f(b)}] ⊆ f([a,b]).

LaTeX

$$[min{f(a),f(b)}, max{f(a),f(b)}] ⊆ f([a,b])$$

Lean4

/-- **Intermediate Value Theorem** for continuous functions on closed intervals, unordered case. -/
theorem intermediate_value_uIcc {a b : α} {f : α → δ} (hf : ContinuousOn f [[a, b]]) : [[f a, f b]] ⊆ f '' uIcc a b :=
  by cases le_total (f a) (f b) <;> simp [*, isPreconnected_uIcc.intermediate_value]

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