summable_ofReal — Mathlib

English

For any f: α → ℝ, the real-valued family is summable with respect to L in ℝ if and only if its image in 𝕜 is summable, i.e., Summable (fun x => (f x : 𝕜)) L ↔ Summable f L.

Русский

Для любого f: α → ℝ свёртываемость ряда сохраняется при вложении вещественных чисел в 𝕜: Summable (f x : 𝕜) эквивалентно Summable f.

LaTeX

$$$ \\Summable (a \\mapsto (f(a) : \\mathbb{K})) L \\iff \\Summable f L $$$

Lean4

@[simp, norm_cast]
theorem summable_ofReal {f : α → ℝ} : Summable (fun x => (f x : 𝕜)) L ↔ Summable f L :=
  ⟨fun h => by simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.summable h, ofRealCLM.summable⟩

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