tendsto_comp_coe_Ioi_atBot — Mathlib

English

If a β→ Ioi(a) is considered, Tendsto from atBot is equivalent to Tendsto of f at the right neighborhood of a.

Русский

Если смотреть на Ioi(a), то пределы от atBot равны пределу f в окрестности справа от a.

LaTeX

$$$\\mathrm{Tendsto}(f)\\;\\mathrm{atBot} \\iff \\mathrm{Tendsto}(f)\\;\\mathcal{N}_{>}(a)$$$

Lean4

@[simp]
theorem tendsto_comp_coe_Ioi_atBot : Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioi_atBot, tendsto_map'_iff]; rfl

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