English
If E is a group with a norm and a left-translation invariant pseudodistance dist'(x,y) ≤ dist'(x z, y z) and ∥x∥ = dist'(x,1), then dist'(x,y) = ∥x y^{-1}∥ defines a SeminormedGroup structure.
Русский
Если есть псевдорасстояние dist'(x,y) ≤ dist'(x z, y z) удовлетворяющее ∥x∥ = dist'(x,1), то dist'(x,y) = ∥x y^{-1}∥ задаёт SeminormedGroup.
LaTeX
$$$\forall x,y,z, dist'(x,y) \le dist'(x z,y z)$ and $‖x‖ = dist'(x,1) \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] [Group E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : SeminormedGroup E where
dist_eq x
y := by
rw [h₁]; apply le_antisymm
· simpa only [div_mul_cancel, one_mul] using h₂ (x / y) 1 y
·
simpa only [div_eq_mul_inv, ← mul_inv_cancel y] using
h₂ _ _
_
-- See note [reducible non-instances]
