tendsto_comp_val_Ioi_atTop — Mathlib

English

For f: α → β and l a filter, Tendsto (λ x: Ici a => f x) atTop l is equivalent to Tendsto f atTop l.

Русский

Для f: α → β и фильтра l, Tendsto (f на область Ici a) в atTop равносильно Tendsto f в atTop.

LaTeX

$$$\mathrm{Tendsto}\ (\lambda x:\mathsf{Ici}(a).\ x \mapsto f x)\ \mathrm{atTop}\ l \iff \mathrm{Tendsto}\ f\ \mathrm{atTop}\ l$$$

Lean4

@[simp]
theorem tendsto_comp_val_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] {a : α} {f : α → β}
    {l : Filter β} : Tendsto (fun x : Ioi a => f x) atTop l ↔ Tendsto f atTop l := by
  rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]

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