α : Type u_1
β : Type ?u.245507
γ : Type ?u.245510
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g a : α → ℝ≥0∞
j : α
h : ⊤ ≤ a j
⊢ (∑' (i : α), a i) = ⊤
α : Type u_1
β : Type ?u.245507
γ : Type ?u.245510
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g a : α → ℝ≥0∞
tsum_ne_top : (∑' (i : α), a i) ≠ ⊤
j : α
⊢ a j < ⊤
contrapose! tsum_ne_top with h
no goals
α : Type u_1
β : Type ?u.245507
γ : Type ?u.245510
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g a : α → ℝ≥0∞
j : α
h : ⊤ ≤ a j
⊢ (∑' (i : α), a i) = ⊤
exact ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩