English
If a densely ordered codomain f is strictly monotone on a right neighborhood and the image is dense enough to meet/cover intervals approaching f(a), then f is continuous at a from the right.
Русский
Если кодом denselyOrdered β норма f строго монотонна на правой окрестности и образ плотный по мере подхода к f(a), тогда f непрерывна справа в a.
LaTeX
$$$\text{StrictMonoOn}(f, s) \wedge s \in \mathcal{N}[\ge] a \wedge (closure (f'' s) \in \mathcal{N}[\ge] f(a)) \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Ici}(a), a)$$$
Lean4
/-- If a function `f` with a densely ordered codomain is 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_monotoneOn_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α}
{a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : f '' s ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a :=
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs <| mem_of_superset hfs subset_closure
