tendsto_leftLim_within — Mathlib

English

If f is antitone, then f tends to the left limit within x from the left to leftLim f x, i.e., Tendsto f (nhdsWithin x (Iio x)) (nhdsWithin (leftLim f x) (Ici (leftLim f x))).

Русский

Если f антимонотонна, то из левой окрестности x функция сходится к левому пределу: Tendsto f (nhdsWithin x (Iio x)) (nhdsWithin (leftLim f x) (Ici (leftLim f x))).

LaTeX

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

Lean4

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

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