English
A seminormed commutative group is a uniform group; multiplication and division are uniformly continuous.
Русский
Полугруппа с нормой является равномерной группой; умножение и деление непрерывны в рамках равномерной структуры.
LaTeX
$$$\\text{IsUniformGroup}(E)$ for a seminormed commutative group E;\\; \\text{uniform continuous}(\\cdot,\\cdot).$$$
Lean4
/-- A seminormed group is a uniform group, i.e., multiplication and division are uniformly
continuous. -/
@[to_additive /-- A seminormed group is a uniform additive group, i.e., addition and subtraction are
uniformly continuous. -/
]
instance (priority := 100) to_isUniformGroup : IsUniformGroup E :=
⟨(LipschitzWith.prod_fst.div LipschitzWith.prod_snd).uniformContinuous⟩
-- short-circuit type class inference
-- See note [lower instance priority]
