English
Let a ≤ b and f be continuous on [a, b]. Then every y with f(b) < y ≤ f(a) appears as f(x) for some x in [a, b). In particular, Ioc(f(b), f(a)) ⊆ f(Ico(a, b)).
Русский
Пусть a ≤ b и f непрерывна на [a, b]. Тогда каждое y, удовлетворяющее f(b) < y ≤ f(a), встречается как значение f в некоторой точке x ∈ [a, b).
LaTeX
$$$Ioc\\left(f(b), f(a)\\right) \\subseteq f\\left(Ico(a, b)\\right)$$$
Lean4
theorem intermediate_value_Ico' {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
Ioc (f b) (f a) ⊆ f '' Ico a b :=
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_ge (he ▸ h.2))) fun hlt =>
@IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ico _ _ ⟨refl a, hlt⟩
(right_nhdsWithin_Ico_neBot hlt) inf_le_right _ (hf.mono Ico_subset_Icc_self) _
((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ico_subset_Icc_self)
