LSeriesHasSum_congr — Mathlib

English

If f and g agree away from zero (n ≠ 0 implies f(n) = g(n)), then LSeriesHasSum f s a ↔ LSeriesHasSum g s a.

Русский

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

LaTeX

$$∀ {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n), LSeriesHasSum f s a ↔ LSeriesHasSum g s a$$

Lean4

theorem LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
    LSeriesHasSum f s a ↔ LSeriesHasSum g s a := by
  simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr h s]

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