English
Let f be monotone on a neighborhood s of a. If for every b < f(a) there exists c ∈ s with f(c) ∈ Ioo(b, f(a)) and for every b > f(a) there exists c ∈ s with f(c) ∈ Ioo (f(a), b), then f is continuous at a: ContinuousAt f a.
Русский
Пусть f монотонна на окрестности s точки a. Если для любого b<f(a) существует c∈s с f(c)∈Ioo(b,f(a)) и для любого b>f(a) существует c∈s с f(c)∈Ioo(f(a),b), тогда f непрерывна в a.
LaTeX
$$$(\\forall b< f(a), \\exists c \\in s, f(c) \\in Ioo(b,f(a))) \\land (\\forall b> f(a), \\exists c \\in s, f(c) \\in Ioo (f(a), b)) \\Rightarrow ContinuousAt f a.$$$
Lean4
/-- If `f` is a monotone function on a neighborhood of `a` and the image of this neighborhood under
`f` meets every interval `(b, f a)`, `b < f a`, and every interval `(f a, b)`, `b > f a`, then `f`
is continuous at `a`. -/
theorem continuousAt_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s)
(hs : s ∈ 𝓝 a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) :
ContinuousAt f a :=
continuousAt_iff_continuous_left_right.2
⟨continuousWithinAt_left_of_monotoneOn_of_exists_between h_mono (mem_nhdsWithin_of_mem_nhds hs) hfs_l,
continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩
