English
If f is monotone, then Tendsto to leftLim or rightLim along left or right neighborhoods holds, respectively.
Русский
Если f монотонна, то существуют предельные переходы к leftLim слева и к rightLim справа вдоль соответствующих окрестностей.
LaTeX
$$$\text{Monotone}(f) \Rightarrow \operatorname{tendsto}(f, \mathcal{N}_{<}(a), \mathcal{N}(\operatorname{leftLim}(f,a))) \text{ и } \operatorname{tendsto}(f, \mathcal{N}_{>}(a), \mathcal{N}(\operatorname{rightLim}(f,a)))$$$
Lean4
theorem rightLim_le_leftLim (h : x < y) : rightLim f x ≤ leftLim f y :=
by
letI : TopologicalSpace α := Preorder.topology α
haveI : OrderTopology α := ⟨rfl⟩
rcases eq_or_neBot (𝓝[<] y) with (h' | h')
· simpa [leftLim, h'] using rightLim_le hf h
obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty := nonempty_of_mem (Ioo_mem_nhdsLT h)
calc
rightLim f x ≤ f a := hf.rightLim_le xa
_ ≤ leftLim f y := hf.le_leftLim ay
