@[simp]

theorem ENNReal.prod_eq_top {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} : ∏ i ∈ s, f i = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0