English
If f is strictly monotone on a right neighborhood and its image covers Ioi (f a), then f is continuous at a from the right.
Русский
Если f строго монотонна на правой окрестности и образ покрывает Ioi(f(a)), то f непрерывна справа в a.
LaTeX
$$$\text{StrictMonoOn}(f, s) \Rightarrow \text{nhdsWithin}(a, \mathrm{Ici}(a)) \wedge \text{SurjOn}(f, s, \mathrm{Ioi}(f(a))) \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Ici}(a), a)$$$
Lean4
/-- If `f` is a strictly monotone function on a left neighborhood of `a` and the image of this
neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, then `f` is continuous at `a`
from the left.
The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x < 0 then x else x + 1` would be a counter-example at
`a = 0`. -/
theorem continuousWithinAt_left_of_exists_between {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s)
(hs : s ∈ 𝓝[≤] a) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)) : ContinuousWithinAt f (Iic a) a :=
h_mono.dual.continuousWithinAt_right_of_exists_between hs fun b hb =>
let ⟨c, hcs, hcb, hca⟩ := hfs b hb
⟨c, hcs, hca, hcb⟩
