tendsto_rightLim_within — Mathlib

English

For monotone f, Tendsto f (nhdsWithin x (Ioi x)) (nhds (rightLim f x))

Русский

Для монотонной f имеет место стремление к правой границе: Tendsto f (nhdsWithin x (Ioi x)) (nhds (rightLim f x)).

LaTeX

$$$\operatorname{Tendsto}(f, \mathcal{N}_{Within}(x, \mathrm{Ioi}(x)), \mathcal{N}(\operatorname{rightLim}(f,x)))$$$

Lean4

theorem tendsto_rightLim_within (x : α) : Tendsto f (𝓝[>] x) (𝓝[≥] rightLim f x) :=
  hf.dual.tendsto_leftLim_within x

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