not_tendsto_const_atTop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem not_tendsto_const_atTop [Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot] :
    ¬Tendsto (fun _ => x) l atTop :=
  tendsto_const_pure.not_tendsto (disjoint_pure_atTop x)

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