no goals
α : Type ?u.720562
β : Type ?u.720565
ι : Type ?u.720568
E : Type ?u.720571
F : Type ?u.720574
𝕜 : Type ?u.720577
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Memℒp f p
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}
simp
no goals
α : Type ?u.720562
β : Type u_2
ι : Type ?u.720568
E : Type u_1
F : Type ?u.720574
𝕜 : Type ?u.720577
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Memℒp f p
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}
simp