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