eventually_ne_of_tendsto_norm_atTop'

English

If ‖f y‖ → ∞ along a filter l, then for any fixed x, eventually f y ≠ x.

Русский

Если ‖f y‖ → ∞ вдоль фильтра l, то для любого фиксированного x позднее неравно f y ≠ x.

LaTeX

$$$ \text{Tendsto}( \lambda y, \|f y\|, l, \text{atTop}) \Rightarrow \forall x, \forall^\infty y, f y \neq x. $$$

Lean4

/-- If `‖y‖ → ∞`, then we can assume `y ≠ x` for any fixed `x`. -/
@[to_additive eventually_ne_of_tendsto_norm_atTop /-- If `‖y‖→∞`, then we can assume `y≠x` for any
    fixed `x` -/
    ]
theorem eventually_ne_of_tendsto_norm_atTop' {l : Filter α} {f : α → E} (h : Tendsto (fun y => ‖f y‖) l atTop) (x : E) :
    ∀ᶠ y in l, f y ≠ x :=
  (h.eventually_ne_atTop _).mono fun _x => ne_of_apply_ne norm

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