tendsto_leftLim_within — Mathlib

English

For monotone f, Tendsto f (nhdsWithin x (Iio x)) (nhdsWithin (leftLim f x) (Iic (leftLim f x))) holds.

Русский

Для монотонной f имеем схождение вдоль nhdsWithin x Iio x к leftLim f x в рамках nhdsWithin (leftLim f x) Iic (leftLim f x).

LaTeX

$$$\operatorname{Tendsto}(f, \mathcal{N}_{Within}(x, \mathrm{Iio}(x)), \mathcal{N}_{Within}(\operatorname{leftLim}(f,x), \mathrm{Iic}(\operatorname{leftLim}(f,x))))$$$

Lean4

theorem tendsto_leftLim_within (x : α) : Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x) :=
  by
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)
  filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy

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