LSeriesSummable_congr — Mathlib

English

If f and g agree on all n ≠ 0, then LSeriesSummable f s ↔ LSeriesSummable g s.

Русский

Если f и g совпадают для всех n ≠ 0, то LSeriesSummable f s эквивалентно LSeriesSummable g s.

LaTeX

$$$\\bigl(\\forall n\\, (n \\neq 0 \\Rightarrow f(n) = g(n))\\bigr) \\Rightarrow (LSeriesSummable(f,s) \\leftrightarrow LSeriesSummable(g,s))$$$

Lean4

theorem LSeriesSummable_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
    LSeriesSummable f s ↔ LSeriesSummable g s :=
  summable_congr <| term_congr h s

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