English
Let β be a preorder with no minimum element. If a function f from α to β tends to the bottom along a filter l (i.e., f(l) approaches atBot), then the image of f is not bounded below along l.
Русский
Пусть β упорядочено с отношением порядка без минимального элемента. Если функция f: α → β стремится к наименьшему элементу вдоль фильтра l, то образ f не ограничен снизу вдоль l.
LaTeX
$$$\text{Let } (\beta, \le) \text{ be a preorder with no minimum element } f: \alpha \to \beta, \text{ and } l \text{ a filter on } \alpha. \\ \\ \text{If } \operatorname{Tendsto} f\, l\, \operatorname{atBot}, \text{ then } \neg \exists b \in \beta, \forall^{\infty}_{a \in l} \ f(a) \ge b.$$$
Lean4
theorem not_isBoundedUnder_of_tendsto_atBot [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} [l.NeBot]
(hf : Tendsto f l atBot) : ¬IsBoundedUnder (· ≥ ·) l f :=
not_isBoundedUnder_of_tendsto_atTop (β := βᵒᵈ) hf
