leftLim_eq_sSup — Mathlib

English

For a monotone function f, leftLim f x equals the supremum of the image of f on the left side Iio x, i.e. leftLim f x = sSup (f'' Iio x).

Русский

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

LaTeX

$$$\operatorname{leftLim}(f,x) = \operatorname{sSup}(f''(\mathrm{Iio}(x)))$$$

Lean4

theorem leftLim_eq_sSup [TopologicalSpace α] [OrderTopology α] (h : 𝓝[<] x ≠ ⊥) : leftLim f x = sSup (f '' Iio x) :=
  leftLim_eq_of_tendsto h (hf.tendsto_nhdsLT x)

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