English
If f is monotone on Ioi x and image is bounded below, Tendsto to sInf of image from the right.
Русский
Если f монотонна на Ioi x и образ ограничен снизу, то сходится к sInf образа справа.
LaTeX
$$$\mathrm{MonotoneOn}(f, Ioi(x)) \Rightarrow \mathrm{BddBelow}(f'' Ioi(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Ioi(x))))$$$
Lean4
/-- If `f` is a monotone function on a right neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(f a, b)`, `b > f a`, then `f` is continuous at `a` from the right.
The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b` cannot be replaced by the weaker
assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` we use for strictly monotone functions
because otherwise the function `ceil : ℝ → ℤ` would be a counter-example at `a = 0`. -/
theorem continuousWithinAt_right_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α}
(h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) :
ContinuousWithinAt f (Ici a) a := by
have ha : a ∈ Ici a := left_mem_Ici
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
· filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le (h_mono has hxs hxa)
· rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
have : a < c := not_le.1 fun h => hac.not_ge <| h_mono hcs has h
filter_upwards [hs, Ico_mem_nhdsGE this]
rintro x hx ⟨_, hxc⟩
exact (h_mono hx hcs hxc.le).trans_lt hcb
