English
Let s be a preconnected subset of a topological space X, f:X→α continuous on s, with v∈α and l1,l2 nontrivial filters on X such that f(l1)→atBot and f(l2)→v. Then every value below v is attained on s; equivalently, (−∞, v) ⊆ f(s).
Русский
Пусть s ⊆ X неприводимо связно, f: X → α непрерывна на s, и пределы f по l1 и l2 достигают atBot и v соответственно. Тогда все значения меньше v достигаются на 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 Iio(v) \subseteq f''s$$$
Lean4
theorem intermediate_value_Iio {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₁ atBot)
(ht₂ : Tendsto f l₂ (𝓝 v)) : Iio v ⊆ f '' s := fun y h =>
hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
(ht₂.eventually_const_le h)
