English
Let α be a preorder directed by ≥. For any a ∈ α, any function f: α → β, and any filter l on β, the limit of f along atBot after restricting the domain to the lower set {x ∈ α : x ≤ a} is equivalent to the limit of f along atBot on α. In symbols, Tendsto (x ↦ f x) on Iic(a) toward l atBot l if and only if Tendsto f toward l atBot l.
Русский
Пусть α — частично упорядоченное множество направлено по отношению ≥. Для любого a ∈ α, любой отображение f: α → β и любого фильтра l на β предел f по atBot после ограничения области до множества {x ∈ α | x ≤ a} равен пределу f по atBot на α. Формально: Tendsto (x ↦ f x) на Iic(a) к l тогда и только тогда, когда Tendsto f к l на atBot.
LaTeX
$$$$\operatorname{Tendsto}\left(f|_{(-\infty,a]}\right)\_{\text{atBot } l} \;\Longleftrightarrow\; \operatorname{Tendsto} f\_{\text{atBot } l}$$$$
Lean4
@[simp]
theorem tendsto_comp_val_Iic_atBot [Preorder α] [IsDirected α (· ≥ ·)] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun x : Iic a => f x) atBot l ↔ Tendsto f atBot l :=
tendsto_comp_val_Ici_atTop (α := αᵒᵈ)
