α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1167772
G : Type ?u.1167775
𝕜 : Type u_4
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑(setToL1' 𝕜 hT h_smul) (c • f) = c • ↑(setToL1' 𝕜 hT h_smul) f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1167772
G : Type ?u.1167775
𝕜 : Type u_4
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑(setToL1 hT) (c • f) = c • ↑(setToL1 hT) f
rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1167772
G : Type ?u.1167775
𝕜 : Type u_4
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑(setToL1' 𝕜 hT h_smul) (c • f) = c • ↑(setToL1' 𝕜 hT h_smul) f
exact ContinuousLinearMap.map_smul _ _ _