tendsto_zero_smul_of_tendsto_zero_of_bounded

English

If ε_n → 0 in 𝕜 and g_n is bounded in norm, then ε_n · g_n → 0 in 𝔸.

Русский

Если ε_n → 0 в 𝕜 и ||g_n|| ограничено, то ε_n · g_n → 0 в 𝔸.

LaTeX

$$$ \\text{Tendsto } \\varepsilon \\ l (\\mathcal{N} 0) \\Rightarrow \\text{Tendsto } (\\varepsilon \\cdot g) \\ l (\\mathcal{N} 0) $$$

Lean4

/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
theorem tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*} [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸]
    [Module 𝕜 𝔸] [IsBoundedSMul 𝕜 𝔸] {l : Filter ι} {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Tendsto ε l (𝓝 0))
    (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) : Tendsto (ε • f) l (𝓝 0) :=
  by
  rw [← isLittleO_one_iff 𝕜] at hε ⊢
  simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))

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