English
If E is a group with a norm and left invariant pseudodistance dist', then dist'(x,y) ≤ dist'(x z, y z) and dist'(x,y) = ∥x y^{-1}∥ yields a NormedGroup structure with eq_of_dist_eq_zero given appropriately.
Русский
Если E — группа с нормой и левоинвариантным псевдорdistance dist', то dist'(x,y) ≤ dist'(x z, y z) и dist'(x,y) = ∥x y^{-1}∥ образуют структуру NormedGroup с нужным eq-условием.
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] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : NormedGroup E :=
{ SeminormedGroup.ofMulDist' h₁ h₂ with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
-- See note [reducible non-instances]
