no goals
ι : Type u_2
κ : Type ?u.62135
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), abs (f ↑x) = f ↑x
h2 : ∀ (x : ↑(sᶜ)), abs (f ↑x) = -f ↑x
⊢ ((Summable fun x => abs (f ↑x)) ∧ Summable fun x => abs (f ↑x)) ↔ (Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x
simp only [h1, h2]
no goals
ι : Type u_2
κ : Type ?u.62135
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), abs (f ↑x) = f ↑x
h2 : ∀ (x : ↑(sᶜ)), abs (f ↑x) = -f ↑x
⊢ ((Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x) ↔ Summable f
simp only [summable_neg_iff, summable_subtype_and_compl]