tendsto_Iic_atBot — Mathlib

English

The tendsto along Iic a to atBot is equivalent to tendsto of the embedded value to atBot in the ambient order.

Русский

Сходимость по Iic a к atBot эквивалентна сходимости в двойственном порядке по вложенному значению.

LaTeX

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

Lean4

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

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