English
Let f : α → β be strictly monotone on a left neighborhood s of a, with s ∈ nhds[≤] a, and the image f''s includes Iio (f(a)); then f is continuous from the left at a: ContinuousWithinAt f (Iic a) a.
Русский
Пусть f : α → β строго монотонна на левой окрестности s точки a, причем s является левой окрестностью a, и образ f''s охватывает Iio(f(a)); тогда f непрерывна слева в a: ContinuousWithinAt f (Iic a) a.
LaTeX
$$$ [DenselyOrdered \\beta] \\Rightarrow (StrictMonoOn f s \\land s \\in nhdsWithin a) \\land SurjOn f s (Iio (f a)) \\Rightarrow ContinuousWithinAt f (Iic a) a. $$$
Lean4
/-- If a function `f` is strictly monotone on a left neighborhood of `a` and the image of this
neighborhood under `f` includes `Iio (f a)`, then `f` is continuous at `a` from the left. -/
theorem continuousWithinAt_left_of_surjOn {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a)
(hfs : SurjOn f s (Iio (f a))) : ContinuousWithinAt f (Iic a) a :=
h_mono.dual.continuousWithinAt_right_of_surjOn hs hfs
