no goals
F : Type ?u.1017678
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖f‖ = ⨆ (x : α), ‖↑f x‖
simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]