tendsto_rightLim — Mathlib

English

Analogous tendsto_rightLim_within holds: Tendsto f (nhdsWithin x (Ioi x)) (nhdsWithin (rightLim f x) (Ici (rightLim f x))).

Русский

Аналогично выполняется tendsto_rightLim_within: предел вдоль nhdsWithin x по Ioi x сходится к правой границе функции.

LaTeX

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

Lean4

theorem tendsto_rightLim (x : α) : Tendsto f (𝓝[>] x) (𝓝 (rightLim f x)) :=
  hf.dual.tendsto_leftLim x

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