English
On a preconnected set s, the image of the open interval Ioo(v1,v2) contains a portion of f''(s) for appropriate f and endpoints v1,v2.
Русский
На предсоединенном множестве s образ открытого интервала Ioo(v1,v2) содержит часть образа f(s).
LaTeX
$$$Ioo(v_1,v_2) \\subseteq f''(s).$$$
Lean4
theorem intermediate_value_Ioo {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂]
(hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v₁ v₂ : α} (ht₁ : Tendsto f l₁ (𝓝 v₁))
(ht₂ : Tendsto f l₂ (𝓝 v₂)) : Ioo v₁ v₂ ⊆ f '' s := fun _ h =>
hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_const h.1)
(ht₂.eventually_const_le h.2)