English
If E is a group with a norm ∥·∥ and a left-translation invariant distance dist with ∥x∥ = dist(x,1) for all x, and dist(x,y) ≤ dist(xz,yz) for all x,y,z, then dist(x,y) = ∥x y^{-1}∥ defines a seminormed group structure on E.
Русский
Если E — группа с нормой ∥·∥ и расстоянием dist, удовлетворяющим инвариантности по левому переносу и свойствам ∥x∥ = dist(x,1) и dist(x,y) ≤ dist(xz,yz), тогда dist(x,y) = ∥x y^{-1}∥ задаёт структуру SeminormedGroup на E.
LaTeX
$$$\text{If } (E,‖·‖,dist)\text{ satisfy } ‖x‖=dist(x,1)\text{ and } dist(x,y)\le dist(xz,yz) \ (\forall x,y,z),\; dist(x,y)=‖x y^{-1}‖$, then a SeminormedGroup structure exists on E.$$
Lean4
/-- Construct a seminormed group from a multiplication-invariant distance. -/
@[to_additive /-- Construct a seminormed group from a translation-invariant distance. -/
]
abbrev ofMulDist [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : SeminormedGroup E where
dist_eq x
y := by
rw [h₁]; apply le_antisymm
· simpa only [div_eq_mul_inv, ← mul_inv_cancel y] using h₂ _ _ _
· simpa only [div_mul_cancel, one_mul] using h₂ (x / y) 1 y
