English
Let s be a preconnected subset of a topological space X, f a function X → α continuous on s, and v ∈ α. If l1, l2 are nontrivial filters on X that are supported on s and f(l1) → v, f(l2) → ∞, then every value above v is attained by f on s; equivalently, (v, ∞) ⊆ f(s).
Русский
Пусть s ⊆ X неприводимо связно, f: X → α непрерывна на s, и v ∈ α. При выполняющихся заданных условиях пределы f по l1 и l2 достигают v и +∞, тогда все значения больше v достигаются на s.
LaTeX
$$$\Big( \text{IsPreconnected}(s) \land \text{ContinuousOn}(f,s) \land (\forall l\,\text{NeBot}(l) \Rightarrow l \le \mathcal P s) \land (\text{Tendsto}(f,l_1,\mathcal N v) \land \text{Tendsto}(f,l_2,\text{atTop})) \Big) \Rightarrow Ioi(v) \subseteq f''s$$$
Lean4
theorem intermediate_value_Ioi {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) {v : α} (ht₁ : Tendsto f l₁ (𝓝 v))
(ht₂ : Tendsto f l₂ atTop) : Ioi v ⊆ f '' s := fun y h =>
hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_const h)
(ht₂.eventually_ge_atTop y)
