English
Let α be a nonempty directed preorder with the reverse-directedness given by ≥, and β be a preorder. For any function f: α → β, f tends to the bottom along atBot if and only if for every b in β there exists an index i in α such that for all a ≤ i we have f(a) ≤ b.
Русский
Пусть α—непустое направленное частично упорядоченное множество с направленностью по отношению ≥, и β—частично упорядоченное множество. Для любой функции f: α → β предел f при снижающемся направлении в α достигает нуля тогда и только если для каждого b ∈ β существует элемент i ∈ α такой, что для всех a ≤ i выполняется f(a) ≤ b.
LaTeX
$$$\mathrm{Tendsto}\ f\ atBot\ atBot \iff \forall b:\beta, \exists i:\alpha, \forall a:\alpha, a \le i \rightarrow f(a) \le b$$$
Lean4
theorem tendsto_atBot_atBot : Tendsto f atBot atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, a ≤ i → f a ≤ b :=
tendsto_atTop_atTop (α := αᵒᵈ) (β := βᵒᵈ)
