abscissaOfAbsConv_congr — Mathlib

English

If two functions f and g agree at every n ≠ 0, then their abscissae of absolute convergence coincide: abscissaOfAbsConv f = abscissaOfAbsConv g.

Русский

Если две функции f и g совпадают при каждом аргументе n ≠ 0, то их абсциссы абсолютной сходимости совпадают.

LaTeX

$$$\\forall f,g:\\mathbb{N}\\to\\mathbb{C},\\; (\\forall n\\neq 0,\\; f(n)=g(n)) \\Rightarrow \\operatorname{abscissaOfAbsConv}(f)=\\operatorname{abscissaOfAbsConv}(g).$$$

Lean4

theorem abscissaOfAbsConv_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) :
    abscissaOfAbsConv f = abscissaOfAbsConv g :=
  congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr x h

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