English
If E is a commutative group with a norm and a left-translation invariant distance dist', then dist'(x,y) ≤ dist'(x z, y z) and dist'(x,y) = ∥x y^{-1}∥ define a NormedCommGroup.
Русский
Если E — коммутативная группа с нормой и слева сохраняемым расстоянием dist', то dist'(x,y) ≤ dist'(x z, y z) и dist'(x,y) = ∥x y^{-1}∥ образуют NormedCommGroup.
LaTeX
$$$\forall x,y,z, dist'(x,y) ≤ dist'(x z,y z) \Rightarrow dist'(x,y)=‖x y^{-1}‖$$$
Lean4
/-- Construct a normed group from a multiplication-invariant pseudodistance. -/
@[to_additive /-- Construct a normed group from a translation-invariant pseudodistance. -/
]
abbrev ofMulDist' [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : NormedCommGroup E :=
{ NormedGroup.ofMulDist' h₁ h₂ with mul_comm := mul_comm }
-- See note [reducible non-instances]
