α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
x : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖x‖ = ↑1 * ‖↑(coeToLp α E ℝ) x‖
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
⊢ ‖setToL1 hT‖ ≤ ↑1 * ‖setToL1SCLM α E μ hT‖
refine'
  ContinuousLinearMap.op_norm_extend_le (setToL1SCLM α E μ hT) (coeToLp α E ℝ)
    (simpleFunc.denseRange one_ne_top) fun x => le_of_eq _
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
x : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖x‖ = ‖↑(coeToLp α E ℝ) x‖
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
x : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖x‖ = ↑1 * ‖↑(coeToLp α E ℝ) x‖
rw [NNReal.coe_one, one_mul]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
x : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖x‖ = ‖↑(coeToLp α E ℝ) x‖
rfl
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1256704
G : Type ?u.1256707
𝕜 : Type ?u.1256710
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
⊢ ↑1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
rw [NNReal.coe_one, one_mul]