English
Let f : α → β be strictly monotone on a neighborhood s of a. If for every b < f(a) there exists c ∈ s with f(c) ∈ Ico(b, f(a)) and for every b > f(a) there exists c ∈ s with f(c) ∈ Ioc (f(a), b), then f is continuous at a: ContinuousAt f a.
Русский
Пусть f : α → β строго монотонна на окрестности s точки a. Если для каждого b < f(a) существует c ∈ s с f(c) ∈ Ico(b, f(a)) и для каждого b > f(a) существует c ∈ s с f(c) ∈ Ioc (f(a), b), то f непрерывна в a: ContinuousAt f a.
LaTeX
$$$\\big( \\forall b < f(a), \\exists c \\in s, f(c) \\in Ico(b,f(a)) \\big) \\land \\big( \\forall b > f(a), \\exists c \\in s, f(c) \\in Ioc (f(a), b) \\big) \\Rightarrow ContinuousAt f a.$$$
Lean4
/-- If a function `f` is strictly monotone 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_exists_between {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a)
(hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) :
ContinuousAt f a :=
continuousAt_iff_continuous_left_right.2
⟨h_mono.continuousWithinAt_left_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_l,
h_mono.continuousWithinAt_right_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩
