English
Let a ≤ b and f be continuous on [a, b]. Then every value y with f(a) ≤ y < f(b) (when f(a) ≤ f(b)) lies in the image of [a, b) under f; equivalently, Ico(f(a), f(b)) ⊆ f(Ico(a, b)).
Русский
Пусть a ≤ b и f непрерывна на отрезке [a, b]. Тогда каждое значение y, удовлетворяющее f(a) ≤ y < f(b) (при условии f(a) ≤ f(b)) принадлежит образу [a, b) при f; эквивалентно Ico(f(a), f(b)) ⊆ f(Ico(a, b)).
LaTeX
$$$Ico\\!\\left(f(a), f(b)\\right) \\subseteq f\\left(Ico\\!\\left(a, b\\right)\\right)$$$
Lean4
theorem intermediate_value_Ico {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
Ico (f a) (f b) ⊆ f '' Ico a b :=
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_ge (he ▸ h.1))) fun hlt =>
@IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ 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)
