tendsto_comp_coe_Ioo_atTop — Mathlib

English

For a function f from the Ioo-interval to β, Tendsto atTop is equivalent to Tendsto of the composed function to the left-neighborhood at b.

Русский

Для функции f: Ioo(a,b) → β равенство предельности на atTop равносильно пределу после композиции к левой окрестности в b.

LaTeX

$$$\\mathrm{Tendsto}(f)\\;\\mathrm{atTop} \\iff \\mathrm{Tendsto}(f\\circ \\mathrm{Subtype.val})\\;\\mathcal{N}_{<}(b)$$$

Lean4

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

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