English
Let s be a preconnected subset of a topological space X, f:X→α continuous on s, and suppose f(l1)→atBot and f(l2)→atTop for nontrivial filters l1,l2 with l1,l2 supported on s. Then the image f(s) is all of α; i.e., univ ⊆ f''s.
Русский
Пусть s непрерывная связная подмножество, f непрерывна на s, пределы на двух фильтрах достигают нижнего и верхнего пределов, тогда образ f(s) заполняет всё множество: f(s)=α.
LaTeX
$$$\Big( \text{IsPreconnected}(s) \land \text{ContinuousOn}(f,s) \land (\text{Tendsto}(f,l_1,\mathrm{nhds}\ v) \land \text{Tendsto}(f,l_2,\mathrm{atTop})) \Big) \Rightarrow \text{univ} \subseteq f''s$$$
Lean4
theorem intermediate_value_Iii {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) (ht₁ : Tendsto f l₁ atBot)
(ht₂ : Tendsto f l₂ atTop) : univ ⊆ f '' s := fun y _ =>
hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
(ht₂.eventually_ge_atTop y)
