tendsto_atBot_mono — Mathlib

English

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

Русский

Если f ≤ g покомпонентно, то Tendsto g l atBot ⇒ Tendsto f l atBot.

LaTeX

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

Lean4

theorem tendsto_atBot_mono [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
    Tendsto g l atBot → Tendsto f l atBot :=
  @tendsto_atTop_mono _ βᵒᵈ _ _ _ _ h

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