English
If a function has a left neighborhood mapping that meets left intervals densely, then continuity on the left holds.
Русский
Если отображение левой окрестности попадает в интервалы слева плотно, то непрерывность слева сохраняется.
LaTeX
$$$\text{MonotoneOn}(f, s) \Rightarrow f'' s \text{ meets left intervals densely} \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 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_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : f '' s ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a :=
continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs (mem_of_superset hfs subset_closure)