English
Let f : α → β be defined on a linearly ordered space α with a densely ordered codomain β and equipped with order-topology. If f is strictly monotone on a left neighborhood s of a, and s is a left neighborhood of a (i.e., s ∈ nhdsWithin a) and the image f''s is a left neighborhood of f(a) (i.e., f''s ∈ nhdsWithin (f a)), then f is continuous from the left at a: ContinuousWithinAt f (Iic a) a.
Русский
Пусть f : α → β, где α упорядочено линейно и β плотно упорядочено, и заданы топологии порядка. Если f строго монотонна на левой окрестности s точки a, и образ s под f образует левую окрестность f(a), то f непрерывна слева в a: ContinuousWithinAt f (Iic a) a.
LaTeX
$$$ [DenselyOrdered \\beta] \\Rightarrow (StrictMonoOn f s \\land s \\in nhdsWithin a (Iic a) \\land Set.image f s \\in nhdsWithin (f(a)) (Iic (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 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_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : f '' s ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a :=
h_mono.dual.continuousWithinAt_right_of_image_mem_nhdsWithin hs hfs
