tendsto_atTop_mono — Mathlib

English

If f ≤ g pointwise, then Tendsto f l atTop implies Tendsto g l atTop.

Русский

Если f ≤ g по всем точкам, то Tendsto f l atTop ⇒ Tendsto g l atTop.

LaTeX

$$$$\forall l, \forall f,g: \alpha \to \beta,\ (\forall n, f(n) \le g(n)) \Rightarrow (\operatorname{Tendsto} f\ l\ atTop \Rightarrow \operatorname{Tendsto} g\ l\ atTop). $$$$

Lean4

theorem tendsto_atTop_mono [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
    Tendsto f l atTop → Tendsto g l atTop :=
  tendsto_atTop_mono' l <| Eventually.of_forall h

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