intermediate_value_Ioc — Mathlib

English

For a preconnected set s, the image of any closed interval Icc(f(a),f(b)) under a continuous map f from s covers a nontrivial portion of the image f''(s).

Русский

Для предсоединенного множества s, образ замкнутого интервала Icc f(a) f(b) охватывает часть образа f(s).

LaTeX

$$$Icc(f(a), f(b)) \\subseteq f(s).$$$

Lean4

theorem intermediate_value_Ioc {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) {v : α} (ht : Tendsto f l (𝓝 v)) : Ioc v (f a) ⊆ f '' s :=
  fun _ h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h.2 (ht.eventually_le_const h.1)).imp fun _ h =>
    h.imp_right Eq.symm

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