no goals
𝓕 : Type ?u.460050
𝕜 : Type ?u.460053
α : Type ?u.460056
ι : Type ?u.460059
κ : Type ?u.460062
E : Type u_1
F : Type ?u.460068
G : Type ?u.460071
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ Continuous fun a => ‖a‖
simpa using continuous_id.dist (continuous_const : Continuous fun _a => (1 : E))