English
Let a ≤ b and f be continuous on [a, b]. Then Ioo(f(b), f(a)) ⊆ f''Ioo(a, b).
Русский
Пусть a ≤ b и f непрерывна на [a, b]. Тогда Ioo(f(b), f(a)) ⊆ f''Ioo(a, b).
LaTeX
$$$Ioo\\left(f(b), f(a)\\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 b) (f a) ⊆ f '' Ioo a b :=
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_gt (he ▸ h.2))) fun hlt =>
@IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _ (right_nhdsWithin_Ioo_neBot hlt)
(left_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _ (hf.mono Ioo_subset_Icc_self) _ _
((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)
((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)
