English
Let α and β be linearly ordered topological spaces with β densely ordered. If a function f: α → β is strictly monotone on a left neighborhood s of a and the closure of f''s is a left neighborhood of f(a), then f is continuous from the left at a.
Русский
Пусть α и β — линейно упорядоченные топологические пространства с плотно упорядоченным β. Если функция f: α → β строго монотонна на левой окрестности s точки a, и замыкание образа f(s) является левой окрестностью точки f(a), то f непрерывна слева в точке a.
LaTeX
$$$[DenselyOrdered\, \beta] \Rightarrow \forall f:\alpha\to\beta\,\forall s\subseteq\alpha\,\forall a:\alpha, \,(StrictMonoOn\, f\, s)\land (s\in 𝓝\_{\le} a)\land (closure(f''s)\in 𝓝\_{\le} f(a)) \Rightarrow \ ContinuousWithinAt\, f\ (Iic\ a)\ a.$$$
Lean4
/-- If a function `f` with a densely ordered codomain is strictly 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_closure_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : closure (f '' s) ∈ 𝓝[≤] f a) :
ContinuousWithinAt f (Iic a) a :=
h_mono.dual.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs hfs
