eventually_ne_atTop' — Mathlib

English

If f tends to infinity, then for every c, eventually the values are not equal to c, even after composition with a certain mapping.

Русский

Если f → бесконечность, то для каждого c после некоторого момента значения не равны c.

LaTeX

$$$$\text{Given } hf : \operatorname{Tendsto} f\ l\ atTop, \; \forall c, \operatorname{Eventual}(x \neq c)\ l.$$$$

Lean4

protected theorem eventually_ne_atTop' [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop)
    (c : α) : ∀ᶠ x in l, x ≠ c :=
  (hf.eventually_ne_atTop (f c)).mono fun _ => ne_of_apply_ne f

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