not_tendsto_const_atBot — Mathlib

English

In any preorder with no bottom element, a constant function cannot tend to the bottom along a nontrivial filter.

Русский

В любом частично упорядоченном множестве без нижнего элемента константная функция не может стремиться к нижнему элементу вдоль ненулевого фильтра.

LaTeX

$$$$\forall x\in \alpha,\; \forall l\; [l \neq \varnothing],\; \neg \operatorname{Tendsto}(\lambda t, x)\; l\; \text{atBot}.$$$$

Lean4

theorem not_tendsto_const_atBot [Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot] :
    ¬Tendsto (fun _ => x) l atBot :=
  tendsto_const_pure.not_tendsto (disjoint_pure_atBot x)

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