α : Type u_2
β : Type ?u.1445144
ι : Type ?u.1445147
E : Type u_1
F : Type ?u.1445153
𝕜 : Type ?u.1445156
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : Memℒp (↑(piecewise s hs (const α c) (const α 0))) p
this : support ↑(const α c) = Set.univ
⊢ ↑↑μ s < ⊤
α : Type u_2
β : Type ?u.1445144
ι : Type ?u.1445147
E : Type u_1
F : Type ?u.1445153
𝕜 : Type ?u.1445156
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : Memℒp (↑(piecewise s hs (const α c) (const α 0))) p
⊢ ↑↑μ s < ⊤
have : Function.support (const α c) = Set.univ := Function.support_const hc
no goals
α : Type u_2
β : Type ?u.1445144
ι : Type ?u.1445147
E : Type u_1
F : Type ?u.1445153
𝕜 : Type ?u.1445156
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : Memℒp (↑(piecewise s hs (const α c) (const α 0))) p
this : support ↑(const α c) = Set.univ
⊢ ↑↑μ s < ⊤
simpa only [memℒp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support,
  support_indicator, Set.inter_univ, this] using hcs