English
For an antitone f, left and right tendsto combine to a left/right limit description around a.
Русский
Для антитонной f левая и правая пределы образуют описание лимита вокруг a.
LaTeX
$$$\mathrm{Antitone}(f) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(a))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(a))))$$$
Lean4
/-- If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f`
is continuous at `a` from the right. -/
theorem continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β}
{s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : closure (f '' s) ∈ 𝓝[≥] f a) :
ContinuousWithinAt f (Ici a) a :=
by
refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_
rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
rcases exists_between hab' with ⟨c', hc'⟩
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with ⟨_, hc, ⟨c, hcs, rfl⟩⟩
exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩
