intermediate_value_Ico — Mathlib

English

In a preconnected set s, with two continuous functions f,g, the image of the half-open interval (v, f(a)) is contained in f''(s) given appropriate tendences.

Русский

Для предсоединенного множества s и двух непрерывных функций f,g в образ полуинтервала (v, f(a)) лежит в f''(s) при заданных условиях стремления.

LaTeX

$$$Ioc(v, f(a)) \\subseteq f''(s).$$$

Lean4

theorem intermediate_value_Ico {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)) : Ico (f a) v ⊆ f '' s :=
  fun _ h => hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h.1 (ht.eventually_const_le h.2)

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