α : Type u_2
E : Type u_1
F : Type ?u.1273342
G : Type ?u.1273345
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Memℒp (fun x => c) p ↔ snorm (fun x => c) p μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.1273342
G : Type ?u.1273345
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Memℒp (fun x => c) p ↔ c = 0 ∨ ↑↑μ Set.univ < ⊤
rw [← snorm_const_lt_top_iff hp_ne_zero hp_ne_top]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.1273342
G : Type ?u.1273345
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Memℒp (fun x => c) p ↔ snorm (fun x => c) p μ < ⊤
exact ⟨fun h => h.2, fun h => ⟨aestronglyMeasurable_const, h⟩⟩