Theorem: ContinuousLinearMap.opNorm_apply_le (ForML/ContinuousLinearMap.lean)

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
⊢ ‖(apply 𝕜 G) u‖ ≤ ‖u‖
Tactic:
rw [opNorm_le_iff (norm_nonneg _)]
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
⊢ ∀ (x : E →L[𝕜] G), ‖((apply 𝕜 G) u) x‖ ≤ ‖u‖ * ‖x‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
⊢ ∀ (x : E →L[𝕜] G), ‖((apply 𝕜 G) u) x‖ ≤ ‖u‖ * ‖x‖
Tactic:
intro c
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖((apply 𝕜 G) u) c‖ ≤ ‖u‖ * ‖c‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖((apply 𝕜 G) u) c‖ ≤ ‖u‖ * ‖c‖
Tactic:
rw [apply_apply, mul_comm]
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖c u‖ ≤ ‖c‖ * ‖u‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖c u‖ ≤ ‖c‖ * ‖u‖
Tactic:
exact le_opNorm c u
State after:
no goals