tendsto_leftLim — Mathlib

English

Analogous tendsto statements hold for tendsto_leftLim and tendsto_rightLim with left and right neighborhoods.

Русский

Аналогичные утверждения о пределностях справедливы для tendsto_leftLim и tendsto_rightLim относительно левых и правых окрестностей.

LaTeX

$$$\operatorname{tendsto}(f,\mathcal{N}_{<}(a), \mathcal{N}(\operatorname{leftLim}(f,a))) \land \operatorname{tendsto}(f,\mathcal{N}_{>}(a), \mathcal{N}(\operatorname{rightLim}(f,a)))$$$

Lean4

theorem tendsto_leftLim (x : α) : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x)) :=
  by
  rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
  · simp [h']
  rw [leftLim_eq_sSup hf h']
  exact hf.tendsto_nhdsLT x

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