intermediate_value_Ici — Mathlib

English

In a preconnected set s, if a ∈ s and f is continuous on s, then the interval [f(a), ∞) lies inside the image f''(s).

Русский

На предсоединенном множестве s, если a ∈ s и f непрерывна на s, то [f(a), ∞) ⊆ f(s).

LaTeX

$$$Ici (f(a)) \\subseteq f''(s).$$$

Lean4

theorem intermediate_value_Ici {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l]
    (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) (ht : Tendsto f l atTop) : Ici (f a) ⊆ f '' s := fun y h =>
  hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h (tendsto_atTop.1 ht y)

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