intermediate_value_Iic — Mathlib

English

For a preconnected set s, the image of the left-closed interval Iic(f(a)) is contained in f(s) given continuity on s and tendsto atBot.

Русский

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

LaTeX

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

Lean4

theorem intermediate_value_Iic {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 atBot) : Iic (f a) ⊆ f '' s := fun y h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h (tendsto_atBot.1 ht y)).imp fun _ h =>
    h.imp_right Eq.symm

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