English
If a densely ordered codomain and strict monotonicity on a left neighborhood ensure that the image’s closure sits in a left neighborhood of f(a), then f is continuous at a from the left.
Русский
При плотном порядке кодом β и строгой монотонности слева получаем непрерывность слева.
LaTeX
$$$\text{StrictMonoOn}(f, s) \Rightarrow s \in \mathcal{N}[\le] a \Rightarrow \mathrm{closure}(f'' s) \in \mathcal{N}[\le] 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 closure of 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_closure_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : closure (f '' s) ∈ 𝓝[≥] f a) :
ContinuousWithinAt f (Ici a) a :=
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin (fun _ hx _ hy => (h_mono.le_iff_le hx hy).2)
hs hfs
