α : Type u_2
β : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)
α : Type u_2
β : Type u_1
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)
rw [← summable_coe] at hf ⊢
no goals
α : Type u_2
β : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)
exact hf.comp_injective hi