tendsto_Ici_atTop — Mathlib

English

For f: β → Ici a, Tendsto f l atTop iff Tendsto f x to α via the underlying value.

Русский

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

LaTeX

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

Lean4

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

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