intermediate_value_Icc' — Mathlib

English

If f is continuous on the unordered closed interval uIcc(a,b), then the image of [a,b] contains the entire unordered interval between f(a) and f(b).

Русский

Если f непрерывна на неупорядоченном замкнутом интервале uIcc(a,b), то образ [a,b] содержит целиком неупорядоченный интервал между f(a) и f(b).

LaTeX

$$[[f a, f b]] ⊆ f '' uIcc a b$$

Lean4

/-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
`f a ≥ t ≥ f b`. -/
theorem intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    Icc (f b) (f a) ⊆ f '' Icc a b :=
  isPreconnected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf

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