eventually_ne_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\ atBot.$$$$

Lean4

protected theorem eventually_ne_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot)
    (c : β) : ∀ᶠ x in l, f x ≠ c :=
  hf.eventually (eventually_ne_atBot c)

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