tendsto_Iio_atBot — Mathlib

English

Similarly, Tendsto f l atBot for f: β → Iio a is equivalent to Tendsto f x.l atBot of the underlying value.

Русский

similarly for Iio a: Tendsto f l atBot ⇔ Tendsto (f x).val l atBot.

LaTeX

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

Lean4

theorem tendsto_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)] {a : α} {f : β → Iio a} {l : Filter β} :
    Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot :=
  tendsto_Ioi_atTop (α := αᵒᵈ)

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