V : Type ?u.470292
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖NormedAddGroupHom.comp g f‖ ≤ C₂ * C₁
V : Type ?u.470292
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖NormedAddGroupHom.comp g f‖ ≤ C₃
rw [h]
no goals
V : Type ?u.470292
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖NormedAddGroupHom.comp g f‖ ≤ C₂ * C₁
exact norm_comp_le_of_le hg hf