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