𝓕 : Type u_1
𝕜 : Type ?u.280047
α : Type ?u.280050
ι : Type ?u.280053
κ : Type ?u.280056
E : Type u_2
F : Type u_3
G : Type ?u.280065
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ (∀ (x y : E), ‖↑f (x / y)‖ = ‖x / y‖) ↔ ∀ (x : E), ‖↑f x‖ = ‖x‖
𝓕 : Type u_1
𝕜 : Type ?u.280047
α : Type ?u.280050
ι : Type ?u.280053
κ : Type ?u.280056
E : Type u_2
F : Type u_3
G : Type ?u.280065
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ Isometry ↑f ↔ ∀ (x : E), ‖↑f x‖ = ‖x‖
simp only [isometry_iff_dist_eq, dist_eq_norm_div, ← map_div]
𝓕 : Type u_1
𝕜 : Type ?u.280047
α : Type ?u.280050
ι : Type ?u.280053
κ : Type ?u.280056
E : Type u_2
F : Type u_3
G : Type ?u.280065
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖↑f (x / y)‖ = ‖x / y‖
x : E
⊢ ‖↑f x‖ = ‖x‖
𝓕 : Type u_1
𝕜 : Type ?u.280047
α : Type ?u.280050
ι : Type ?u.280053
κ : Type ?u.280056
E : Type u_2
F : Type u_3
G : Type ?u.280065
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ (∀ (x y : E), ‖↑f (x / y)‖ = ‖x / y‖) ↔ ∀ (x : E), ‖↑f x‖ = ‖x‖
refine' ⟨fun h x => _, fun h x y => h _⟩
no goals
𝓕 : Type u_1
𝕜 : Type ?u.280047
α : Type ?u.280050
ι : Type ?u.280053
κ : Type ?u.280056
E : Type u_2
F : Type u_3
G : Type ?u.280065
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖↑f (x / y)‖ = ‖x / y‖
x : E
⊢ ‖↑f x‖ = ‖x‖
simpa using h x 1