English
If b ≤ f(x) ≤ B eventually and g(x) → 0, then f(x)g(x) → 0.
Русский
Если bf x ограничено между b и B и g(x) → 0, то f(x)g(x) → 0.
LaTeX
$$Let f, g : α → 𝕜 with b ≤ f(x) ≤ B eventually and g(x) → 0, then f(x)g(x) → 0.$$
Lean4
/-- If `g` tends to zero and there exist constants `b B : 𝕜` such that eventually `b ≤ f x| ≤ B`,
then the product `f * g` tends to zero. -/
theorem bdd_le_mul_tendsto_zero {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B)
(hg : Tendsto g l (𝓝 0)) : Tendsto (fun x ↦ f x * g x) l (𝓝 0) :=
by
set C := max |b| |B|
have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))
have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)
apply bdd_le_mul_tendsto_zero' C _ hg
filter_upwards [hb, hB]
exact fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩
