English
If a function f is strictly monotone on a neighborhood s of a and the image f''s meets both sides of f(a) by intervals [b, f(a)) and (f(a), b], then f is continuous at a: ContinuousAt f a.
Русский
Если f строго монотонна на окрестности s точки a и образ f''s пересекает обе стороны f(a) интервалами [b, f(a)) и (f(a), b], то f непрерывна в a.
LaTeX
$$$(\\forall b< f(a), \\exists c \\in s, f(c) \\in Ico(b,f(a))) \\land (\\forall b> f(a), \\exists c \\in s, f(c) \\in Ioc (f(a), b)) \\Rightarrow ContinuousAt f a.$$$
Lean4
/-- If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the
closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is
continuous at `a`. -/
theorem continuousAt_of_monotoneOn_of_closure_image_mem_nhds [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a) (hfs : closure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a :=
continuousAt_iff_continuous_left_right.2
⟨continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono (mem_nhdsWithin_of_mem_nhds hs)
(mem_nhdsWithin_of_mem_nhds hfs),
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono (mem_nhdsWithin_of_mem_nhds hs)
(mem_nhdsWithin_of_mem_nhds hfs)⟩
