English
If f is monotone, Tendsto to leftLim from the left and to rightLim from the right hold with corresponding nhds.
Русский
Если f монотонна, существуют пределы слева и справа: Tendsto к leftLim слева и к rightLim справа с соответствующими окрестностями.
LaTeX
$$$\operatorname{tendsto}(f, 𝓝[<] x, 𝓝(\operatorname{leftLim}(f,x))) \land \operatorname{tendsto}(f, 𝓝[>] x, 𝓝(\operatorname{rightLim}(f,x)))$$$
Lean4
/-- A monotone function is continuous to the left at a point if and only if its left limit
coincides with the value of the function. -/
theorem continuousWithinAt_Iio_iff_leftLim_eq : ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x :=
by
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
· simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'
refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩
have := hf.tendsto_leftLim x
rwa [h] at this
