rightLim_le — Mathlib

English

A monotone function is continuous at a from both sides if and only if the left and right limits agree with the function value at a.

Русский

Для монотонной функции непрерывность в точке достигается по обоим направлениям, если левая и правая границы совпадают со значением функции в точке.

LaTeX

$$$\operatorname{ContinuousAt}(f,a) \iff (\operatorname{leftLim}(f,a) = f(a)) \land (\operatorname{rightLim}(f,a) = f(a))$$$

Lean4

theorem rightLim_le (h : x < y) : rightLim f x ≤ f y :=
  hf.dual.le_leftLim h

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