English
Let a ≤ b and f be continuous on [a, b]. Then for any y with f(a) ≤ y ≤ f(b), there exists x ∈ [a, b] such that f(x) = y; equivalently, f(Icc(a, b)) ⊇ Icc(f(a), f(b)).
Русский
Пусть a ≤ b и f непрерывна на [a, b]. Для любого y между f(a) и f(b) существует x ∈ [a, b] такое, что f(x) = y; образ множества f на Icc(a,b) содержит Icc(f(a), f(b)).
LaTeX
$$$Icc\\left(f(a), f(b)\\right) \\subseteq f\\left(Icc(a, b)\\right)$$$
Lean4
theorem intermediate_value_Ioc {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
Ioc (f a) (f b) ⊆ f '' Ioc a b :=
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_le_of_gt (he ▸ h.1))) fun hlt =>
@IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
(left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)
