tendsto_Ioi_atTop — Mathlib

English

For f: β → Ioi a, Tendsto f l atTop iff Tendsto (f x).val l atTop.

Русский

Для f: β → Ioi a имеет место эквивалентность: Tendsto f l atTop ⇔ Tendsto (f x).val l atTop.

LaTeX

$$$\mathrm{Tendsto}\ f\ l\ \mathrm{atTop} \iff \mathrm{Tendsto}\left(\lambda x. (f\,x : \alpha)\right)\ l\ \mathrm{atTop}$$$

Lean4

theorem tendsto_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] {a : α} {f : β → Ioi a} {l : Filter β} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop := by
  rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]

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