tendsto_comp_coe_Ioo_atBot — Mathlib

English

Equivalence of tendsto for f from Ioo(a,b) with Tendsto of the component to a from the right.

Русский

Эквивалентность предельности для f: Ioo(a,b) ↦ β и предельности компонентd f(x) в a справа.

LaTeX

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

Lean4

@[simp]
theorem tendsto_comp_coe_Ioo_atBot (h : a < b) : Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioo_atBot h, tendsto_map'_iff]; rfl

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