tendsto_rightLim — Mathlib

English

If f is antitone, then f tends to the right limit at x from the right: Tendsto f (nhdsWithin x (Ioi x)) (nhds (rightLim f x)).

Русский

Если f антимонотонна, то сходится к правому пределу: Tendsto f (nhdsWithin x (Ioi x)) (nhds (rightLim f x)).

LaTeX

$$$\text{Antitone}(f) \Rightarrow \forall x,\, \operatorname{Tendsto} f (\mathcal{nhdsWithin} x (\mathrm{Ioi} x)) (\mathcal{nhds} (\operatorname{rightLim} f x))$$$

Lean4

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

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