rightLim_eq_sInf — Mathlib

English

For a monotone f, rightLim f x equals the infimum of the image of f on the right side Ioi x, i.e. rightLim f x = sInf (f'' Ioi x).

Русский

Для монотонной функции f правая граница в точке x равна инфимуму образа f на множестве Ioi x: rightLim f x = sInf (f'' Ioi x).

LaTeX

$$$\operatorname{rightLim}(f,x) = \operatorname{pInf}(f''(\mathrm{Ioi}(x)))$$$

Lean4

theorem rightLim_eq_sInf [TopologicalSpace α] [OrderTopology α] (h : 𝓝[>] x ≠ ⊥) : rightLim f x = sInf (f '' Ioi x) :=
  rightLim_eq_of_tendsto h (hf.tendsto_nhdsGT x)

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