tendsto_rightLim_within — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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