F : Type ?u.1064401
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖↑f x - ↑g x‖ ≤ ‖f - g‖
F : Type ?u.1064401
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖↑f x - ↑g x‖ ≤ dist f g
rw [dist_eq_norm]
no goals
F : Type ?u.1064401
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖↑f x - ↑g x‖ ≤ ‖f - g‖
exact (f - g).norm_coe_le_norm x