English
Let f be monotone. Then f is continuous at x if and only if the left and right limits at x coincide: leftLim f x = rightLim f x.
Русский
Пусть f монотонна. Тогда f непрерывна в точке x тогда и только когда левые и правые пределы в x совпадают: leftLim f x = rightLim f x.
LaTeX
$$$\text{ContinuousAt}(f,x) \iff \operatorname{leftLim} f x = \operatorname{rightLim} f x$$$
Lean4
/-- A monotone function is continuous at a point if and only if its left and right limits
coincide. -/
theorem continuousAt_iff_leftLim_eq_rightLim : ContinuousAt f x ↔ leftLim f x = rightLim f x :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· have A : leftLim f x = f x := hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
have B : rightLim f x = f x := hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
exact A.trans B.symm
· have h' : leftLim f x = f x := by
apply le_antisymm (leftLim_le hf (le_refl _))
rw [h]
exact le_rightLim hf (le_refl _)
refine continuousAt_iff_continuous_left'_right'.2 ⟨?_, ?_⟩
· exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'
· rw [h] at h'
exact hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'
