no goals
𝓕 : Type ?u.461895
𝕜 : Type ?u.461898
α : Type ?u.461901
ι : Type ?u.461904
κ : Type ?u.461907
E : Type u_1
F : Type ?u.461913
G : Type ?u.461916
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ LipschitzWith 1 norm
simpa only [dist_one_left] using LipschitzWith.dist_right (1 : E)