α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if 0 = 0 then Set.Finite {i | ¬f i = 0}
    else if 0 = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ 0) ↔
    Set.Finite {i | ¬f i = 0}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp f 0 ↔ Set.Finite {i | f i ≠ 0}
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 = 0 then Set.Finite {i | ¬f i = 0}
    else if 0 = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ 0) ↔
    Set.Finite {i | ¬f i = 0}
rw [if_pos rfl]