intermediate_value_Ioo — Mathlib

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)

Похожие утверждения