tendsto_Ioo_atBot — Mathlib

English

Characterization of Tendsto for f: Ioo(a,b) → β to the Ioi/directions from the left endpoint.

Русский

Характеристика предельности для f: Ioo(a,b)→β в окрестностях справа от a.

LaTeX

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

Lean4

@[simp]
theorem tendsto_Ioo_atBot {f : β → Ioo a b} : Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by
  rw [← comap_coe_Ioo_nhdsGT, tendsto_comap_iff]; rfl

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