English
Let f : α → β have densely ordered β, f strictly monotone on s, a ∈ α with s ∈ nhds a and closure(f''s) ∈ nhds (f a). Then f is continuous at a: ContinuousAt f a.
Русский
Пусть β плотно упорядочено, f строго монотонна на s, a ∈ α с s ∈ nhds a и closure(f''s) ∈ nhds (f(a)). Тогда f непрерывна в точке a: ContinuousAt f a.
LaTeX
$$$[DenselyOrdered \\beta] \\Rightarrow (StrictMonoOn f s) (hs : s \\in nhds a) (hfs : closure (f''s) \\in nhds (f a)) \\Rightarrow ContinuousAt f a.$$$
Lean4
/-- If a function `f` with a densely ordered codomain is strictly 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_closure_image_mem_nhds [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
(h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a) (hfs : closure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a :=
continuousAt_iff_continuous_left_right.2
⟨h_mono.continuousWithinAt_left_of_closure_image_mem_nhdsWithin (mem_nhdsWithin_of_mem_nhds hs)
(mem_nhdsWithin_of_mem_nhds hfs),
h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin (mem_nhdsWithin_of_mem_nhds hs)
(mem_nhdsWithin_of_mem_nhds hfs)⟩
