English
Let f : α → β be densely ordered β, f strictly monotone on s. If s ∈ nhds a and f''s ∈ nhds (f a), then f is continuous at a: ContinuousAt f a.
Русский
Пусть f : α → β плотно упорядочено, на s strictly mono. Если s ∈ nhds a и f''s ∈ nhds (f(a)), то f непрерывна в a: ContinuousAt f a.
LaTeX
$$$[DenselyOrdered \\beta] \\Rightarrow (StrictMonoOn f s) (hs : s \\in nhds a) (hfs : 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 image of this set under `f` is a neighborhood of `f a`, then `f` is continuous at `a`. -/
theorem continuousAt_of_image_mem_nhds [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s)
(hs : s ∈ 𝓝 a) (hfs : f '' s ∈ 𝓝 (f a)) : ContinuousAt f a :=
h_mono.continuousAt_of_closure_image_mem_nhds hs (mem_of_superset hfs subset_closure)
