English
Let a ≤ b and f be continuous on [a, b]. Then Ioo(f(a), f(b)) ⊆ f''Ioo(a, b); i.e., every value strictly between f(a) and f(b) is attained at some x with a < x < b.
Русский
Пусть a ≤ b и f непрерывна на [a, b]. Тогда Ioo(f(a), f(b)) ⊆ f''Ioo(a, b); каждое значение между f(a) и f(b) достигается в некоторой точке x ∈ (a, b).
LaTeX
$$$Ioo\\left(f(a), f(b)\\right) \\subseteq f\\left(Ioo(a, b)\\right)$$$
Lean4
theorem intermediate_value_Ioo {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
Ioo (f a) (f b) ⊆ f '' Ioo a b :=
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_gt (he ▸ h.1))) fun hlt =>
@IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _ (left_nhdsWithin_Ioo_neBot hlt)
(right_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _ (hf.mono Ioo_subset_Icc_self) _ _
((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)
((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)
