continuousAt_iff_leftLim_eq_rightLim

English

For a monotone f, continuity at x is equivalent to equality of the left and right limits at x.

Русский

Для монотонной f непрерывность в x эквивалентна равенству левого и правого пределов в x.

LaTeX

$$$\text{ContinuousAt}(f,x) \iff \operatorname{leftLim} f x = \operatorname{rightLim} f x$$$

Lean4

/-- An antitone 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 :=
  hf.dual_right.continuousAt_iff_leftLim_eq_rightLim

Похожие утверждения