English
If f is strictly monotone on a left neighborhood and its image meets every left interval, then f is continuous at a from the left.
Русский
Если f строго монотонна слева от a и образ пересекает каждое левое интервал, то f непрерывна слева в a.
LaTeX
$$$\text{StrictMonoOn}(f, s) \Rightarrow s \in \mathcal{N}[\le] a \Rightarrow (\forall b < f(a), \exists c \in s, f(c) \in Ico(b, f(a))) \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Iic}(a), a)$$$
Lean4
/-- If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood
of `a` and the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is
continuous at `a` from the right. -/
theorem continuousWithinAt_right_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : f '' s ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a :=
h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs (mem_of_superset hfs subset_closure)
