English
If a function is strictly monotone on a left neighborhood and its image contains a left neighborhood of f(a), then f is continuous at a from the left.
Русский
Если f строго монотонна слева от a и образ содержит левую окрестность f(a), то f непрерывна слева в a.
LaTeX
$$$\text{StrictMonoOn}(f, s) \Rightarrow \text{nhdsWithin}(a, \mathrm{Iic}(a))\text{ contains image closure} \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Iic}(a), a)$$$
Lean4
/-- If a function `f` is strictly monotone on a right neighborhood of `a` and the image of this
neighborhood under `f` includes `Ioi (f a)`, then `f` is continuous at `a` from the right. -/
theorem continuousWithinAt_right_of_surjOn {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a)
(hfs : SurjOn f s (Ioi (f a))) : ContinuousWithinAt f (Ici a) a :=
h_mono.continuousWithinAt_right_of_exists_between hs fun _ hb =>
let ⟨c, hcs, hcb⟩ := hfs hb
⟨c, hcs, hcb.symm ▸ hb, hcb.le⟩
