English
Let f be monotone on the open interval Ioo(y,x) with y < x, and suppose f(Ioo(y,x)) is bounded above. Then as the input approaches x from the left, f(t) tends to sSup(f(Ioo(y,x))).
Русский
Пусть f монотонна на открытом интервале Ioo(y,x) с y < x и множество f(Ioo(y,x)) ограничено сверху. Тогда при приближении аргумента к x слева предел f(t) равен sSup(f(Ioo(y,x))).
LaTeX
$$$\\text{If } (Ioo(y,x)) \\neq \\emptyset,\\; f: \\alpha \\to \\beta \\text{ is MonotoneOn on } Ioo(y,x)\\text{ and } BddAbove(f''(Ioo(y,x))), \\\\ \\text{then } \\operatorname{Tendsto} f (\\mathcal{N}_{[<]} x) (\\mathcal{N}(\\sup f''(Ioo(y,x))))$.$$
Lean4
theorem tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α}
(h_nonempty : (Ioo y x).Nonempty) (Mf : MonotoneOn f (Ioo y x)) (h_bdd : BddAbove (f '' Ioo y x)) :
Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x))) :=
by
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
· obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using exists_lt_of_lt_csSup (h_nonempty.image _) hl
filter_upwards [Ioo_mem_nhdsLT zx] with w hw
exact lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le
· rcases h_nonempty with ⟨_, hy, hx⟩
filter_upwards [Ioo_mem_nhdsLT (hy.trans hx)] with w hw
exact (le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm
