α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if ⊤ = 0 then Set.Finite {i | ¬f i = 0}
    else if ⊤ = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ 0) ↔
    BddAbove (Set.range fun i => ‖f i‖)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp f ⊤ ↔ BddAbove (Set.range fun i => ‖f i‖)
dsimp [Memℓp]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if ⊤ = 0 then Set.Finite {i | ¬f i = 0}
    else if ⊤ = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ 0) ↔
    BddAbove (Set.range fun i => ‖f i‖)
rw [if_neg ENNReal.top_ne_zero, if_pos rfl]