α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ snorm (c • ↑↑f) p μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ c • ↑f ∈ Lp E p
rw [mem_Lp_iff_snorm_lt_top, snorm_congr_ae (AEEqFun.coeFn_smul _ _)]
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ ‖c‖₊ • snorm (↑↑f) p μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ snorm (c • ↑↑f) p μ < ⊤
refine' (snorm_const_smul_le _ _).trans_lt _
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ ↑‖c‖₊ < ⊤ ∧ snorm (↑↑f) p μ < ⊤ ∨ ↑‖c‖₊ = 0 ∨ snorm (↑↑f) p μ = 0
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ ‖c‖₊ • snorm (↑↑f) p μ < ⊤
rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_lt_top_iff]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.470041
G : Type ?u.470044
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
𝕜 : Type u_3
𝕜' : Type ?u.470082
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜' E
c : 𝕜
f : { x // x ∈ Lp E p }
⊢ ↑‖c‖₊ < ⊤ ∧ snorm (↑↑f) p μ < ⊤ ∨ ↑‖c‖₊ = 0 ∨ snorm (↑↑f) p μ = 0
exact Or.inl ⟨ENNReal.coe_lt_top, f.prop⟩