tendsto_leftLim — Mathlib

English

If f is antitone, then f tends to the left limit at x when approaching x from the left: Tendsto f (nhdsWithin x (Iio x)) (nhds (leftLim f x)).

Русский

Если f антимонотонна, то при приближении к x слева we have Tendsto f (nhdsWithin x (Iio x)) (nhds (leftLim f x)).

LaTeX

$$$\text{Antitone}(f) \Rightarrow \operatorname{Tendsto} f (\mathcal{nhdsWithin} x (\mathrm{Iio} x)) (\mathcal{nhds} (\operatorname{leftLim} f x))$$$

Lean4

theorem tendsto_leftLim (x : α) : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x)) :=
  hf.dual_right.tendsto_leftLim x

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