English
If a monotone f on a left neighborhood has the closure of its image contained in a left neighborhood of f(a), then f is continuous at a from the left.
Русский
Если монотонная f на левой окрестности имеет замыкание образа, входящее в левую окрестность f(a), то f непрерывна слева в a.
LaTeX
$$$\text{MonotoneOn}(f, s) \Rightarrow \overline{f'' s} \subseteq \mathcal{N}_{[≤]} f(a) \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Iic}(a), a)$$$
Lean4
/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is
continuous at `a` from the left -/
theorem continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α}
{a : α} (hf : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : closure (f '' s) ∈ 𝓝[≤] f a) :
ContinuousWithinAt f (Iic a) a :=
@continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ f s a hf.dual hs hfs
