no goals
α : Type ?u.692725
E : Type ?u.692728
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑μ ∅ ≠ ⊤
simp
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑(indicatorConstLp p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) c) =ᵐ[μ] 0
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ indicatorConstLp p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) c = 0
rw [Lp.eq_zero_iff_ae_eq_zero]
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ 0 = Set.indicator ∅ fun x => c
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑(indicatorConstLp p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) c) =ᵐ[μ] 0
convert indicatorConstLp_coeFn (E := E)
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ 0 = fun x => 0
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ 0 = Set.indicator ∅ fun x => c
simp [Set.indicator_empty']
no goals
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.692731
G : Type ?u.692734
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ 0 = fun x => 0
rfl