summable_coe — Mathlib

English

Summability of (f a : ℝ) is equivalent to summability of f when f maps into NNReal.

Русский

Суммируемость (f a) в ℝ эквивалентна суммируемости f, когда f принимает значения в NNReal.

LaTeX

$$(Summable (λ a, (f a : ℝ)) L) ↔ Summable f L$$

Lean4

@[norm_cast]
theorem summable_coe {f : α → ℝ≥0} : (Summable (fun a => (f a : ℝ)) L) ↔ Summable f L :=
  by
  rcases L.neBot_or_eq_bot with _ | hL
  · constructor
    · exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
    · exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
  · simp [Summable, HasSum, hL]

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