𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
have uni : UniformInducing e := (uniformEmbedding_of_bound _ h_e).toUniformInducing
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
have eq : ∀ x, ψ (e x) = f x := uniformly_extend_of_ind uni h_dense f.uniformContinuous
case pos
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖

case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
by_cases N0 : 0 ≤ N
case pos.refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ 0 ≤ ↑N * ‖f‖

case pos.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ Continuous fun x => ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) x‖

case pos.refine'_3
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ Continuous fun x => ↑N * ‖f‖ * ‖x‖

case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ ∀ (a : E), ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e a)‖ ≤ ↑N * ‖f‖ * ‖↑e a‖
case pos
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
refine' op_norm_le_bound ψ _ (isClosed_property h_dense (isClosed_le _ _) _)
no goals
case pos.refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ 0 ≤ ↑N * ‖f‖
exact mul_nonneg N0 (norm_nonneg _)
no goals
case pos.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ Continuous fun x => ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) x‖
exact continuous_norm.comp (cont ψ)
no goals
case pos.refine'_3
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ Continuous fun x => ↑N * ‖f‖ * ‖x‖
exact continuous_const.mul continuous_norm
case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
x : E
⊢ ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x)‖ ≤ ↑N * ‖f‖ * ‖↑e x‖
case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
⊢ ∀ (a : E), ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e a)‖ ≤ ↑N * ‖f‖ * ‖↑e a‖
intro x
case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
x : E
⊢ ‖↑f x‖ ≤ ↑N * ‖f‖ * ‖↑e x‖
case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
x : E
⊢ ‖↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x)‖ ≤ ↑N * ‖f‖ * ‖↑e x‖
rw [eq]
no goals
case pos.refine'_4
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
x : E
⊢ ‖↑f x‖ ≤ ↑N * ‖f‖ * ‖↑e x‖
calc
  ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_op_norm _ _
  _ ≤ ‖f‖ * (N * ‖e x‖) := (mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _))
  _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]
no goals
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : 0 ≤ N
x : E
⊢ ‖f‖ * (↑N * ‖↑e x‖) ≤ ↑N * ‖f‖ * ‖↑e x‖
rw [mul_comm ↑N ‖f‖, mul_assoc]
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
have he : ∀ x : E, x = 0 := by
  intro x
  have N0 : N ≤ 0 := le_of_lt (lt_of_not_ge N0)
  rw [← norm_le_zero_iff]
  exact le_trans (h_e x) (mul_nonpos_of_nonpos_of_nonneg N0 (norm_nonneg _))
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
have hf : f = 0 := by
  ext x
  simp only [he x, zero_apply, map_zero]
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
hψ : extend f e h_dense (_ : UniformInducing ↑e) = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
have hψ : ψ = 0 := by
  rw [hf]
  apply extend_zero
no goals
case neg
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
hψ : extend f e h_dense (_ : UniformInducing ↑e) = 0
⊢ ‖extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖
rw [hψ, hf, norm_zero, norm_zero, MulZeroClass.mul_zero]
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
x : E
⊢ x = 0
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
⊢ ∀ (x : E), x = 0
intro x
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0✝ : ¬0 ≤ N
x : E
N0 : N ≤ 0
⊢ x = 0
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
x : E
⊢ x = 0
have N0 : N ≤ 0 := le_of_lt (lt_of_not_ge N0)
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0✝ : ¬0 ≤ N
x : E
N0 : N ≤ 0
⊢ ‖x‖ ≤ 0
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0✝ : ¬0 ≤ N
x : E
N0 : N ≤ 0
⊢ x = 0
rw [← norm_le_zero_iff]
no goals
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0✝ : ¬0 ≤ N
x : E
N0 : N ≤ 0
⊢ ‖x‖ ≤ 0
exact le_trans (h_e x) (mul_nonpos_of_nonpos_of_nonneg N0 (norm_nonneg _))
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
x : E
⊢ ↑f x = ↑0 x
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
⊢ f = 0
ext x
no goals
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
x : E
⊢ ↑f x = ↑0 x
simp only [he x, zero_apply, map_zero]
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
⊢ extend 0 e h_dense (_ : UniformInducing ↑e) = 0
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
⊢ extend f e h_dense (_ : UniformInducing ↑e) = 0
rw [hf]
no goals
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.3539330
E : Type u_5
Eₗ : Type ?u.3539336
F : Type u_1
Fₗ : Type u_2
G : Type ?u.3539345
Gₗ : Type ?u.3539348
𝓕 : Type ?u.3539351
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ↑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖
inst✝ : RingHomIsometric σ₁₂
uni : UniformInducing ↑e
eq : ∀ (x : E), ↑(extend f e h_dense (_ : UniformInducing ↑e)) (↑e x) = ↑f x
N0 : ¬0 ≤ N
he : ∀ (x : E), x = 0
hf : f = 0
⊢ extend 0 e h_dense (_ : UniformInducing ↑e) = 0
apply extend_zero