case intro
α : Type u_2
β✝ : Type ?u.346013
γ : Type ?u.346016
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i => ↑(f i)) ↔
    (∀ (x : α), Summable fun y => (fun i => ↑(f i)) { fst := x, snd := y }) ∧
      Summable fun x => ∑' (y : β x), (fun i => ↑(f i)) { fst := x, snd := y }
α : Type u_2
β✝ : Type ?u.346013
γ : Type ?u.346016
β : α → Type u_1
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ Summable f ↔
    (∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }
lift f to (Σx, β x) → ℝ≥0 using hf
no goals
case intro
α : Type u_2
β✝ : Type ?u.346013
γ : Type ?u.346016
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i => ↑(f i)) ↔
    (∀ (x : α), Summable fun y => (fun i => ↑(f i)) { fst := x, snd := y }) ∧
      Summable fun x => ∑' (y : β x), (fun i => ↑(f i)) { fst := x, snd := y }
exact_mod_cast NNReal.summable_sigma