tendsto_mul_iff_of_ne_zero — Mathlib

English

If g tends to y with y ≠ 0, then f n · g n tends to x · y iff f n tends to x.

Русский

Если g_n стремится к y, где y ≠ 0, тогда f_n · g_n стремится к x · y тогда и только тогда, когда f_n стремится к x.

LaTeX

$$\\forall l, f, g: Tendsto g l (\\mathcal{N} y) ∧ y ≠ 0 ⇒ (Tendsto (\\lambda n. f n * g n) l (\\mathcal{N}(x * y)) \\\\iff Tendsto f l (\\mathcal{N} x))$$

Lean4

theorem tendsto_mul_iff_of_ne_zero [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀} (hg : Tendsto g l (𝓝 y))
    (hy : y ≠ 0) : Tendsto (fun n => f n * g n) l (𝓝 <| x * y) ↔ Tendsto f l (𝓝 x) :=
  by
  refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩
  rw [← mul_div_cancel_right₀ x hy]
  refine Tendsto.congr' ?_ (hfg.div hg hy)
  exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

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