α : Type u_1
E : Type ?u.5065049
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ snorm f p μ = 0 ∧ snorm g p μ = 0
α : Type u_1
E : Type ?u.5065049
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ snorm f p μ = 0 ∧ snorm g p μ = 0
simp_rw [le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg (norm_nonneg _) hc (norm_nonneg _),
  norm_eq_zero, eventually_and] at h
α : Type u_1
E : Type ?u.5065049
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0
⊢ snorm f p μ = 0 ∧ snorm g p μ = 0
α : Type u_1
E : Type ?u.5065049
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ snorm f p μ = 0 ∧ snorm g p μ = 0
change f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0 at h
no goals
α : Type u_1
E : Type ?u.5065049
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0
⊢ snorm f p μ = 0 ∧ snorm g p μ = 0
simp [snorm_congr_ae h.1, snorm_congr_ae h.2]