English
Let f: α → β be defined on a nonempty open interval Ioo x y in a ConditionallyCompleteLinearOrder setting, monotone on Ioo x y, and with image f''Ioo x y bounded below. Then f tends to the infimum of f''Ioo x y from the right of x.
Русский
Пусть f: α → β определена на непустом открытом отрезке Ioo x y; она монотонна на Ioo x y и образ f''Ioo x y ограничен снизу. Тогда f стремится к наименьшему элементу множества f''Ioo x y слева от x, т.е. вправо от x.
LaTeX
$$$(Ioo\, x\, y) \neq \emptyset \Rightarrow \text{MonotoneOn}(f, Ioo\, x\, y) \wedge \text{BddBelow}(f''\, Ioo\, x\, y) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\inf(f''\, Ioo\, x\, y)))$$$
Lean4
theorem tendsto_nhdsWithin_Ioo_right {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α}
(h_nonempty : (Ioo x y).Nonempty) (Mf : MonotoneOn f (Ioo x y)) (h_bdd : BddBelow (f '' Ioo x y)) :
Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y))) :=
by
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
· rcases h_nonempty with ⟨p, hy, hx⟩
filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw
exact hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)
· obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
simpa [mem_image, exists_prop, exists_exists_and_eq_and] using exists_lt_of_csInf_lt (h_nonempty.image _) hm
filter_upwards [Ioo_mem_nhdsGT xz] with w hw
exact (Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm
