English
If s is bounded, there exists a positive R such that all x in s satisfy ∥x∥ ≤ R.
Русский
Если s ограничено, существует положительная константа R, такая что для всех x в s выполняется ∥x∥ ≤ R.
LaTeX
$$∃ R > 0, ∀ x ∈ s, ∥x∥ ≤ R$$
Lean4
/-- The (additive) norm on the multiplicative opposite is the same as the norm on the original type.
Note that we do not provide this more generally as `Norm Eᵐᵒᵖ`, as this is not always a good
choice of norm in the multiplicative `SeminormedGroup E` case.
We could repeat this instance to provide a `[SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ` instance,
but that case would likely never be used.
-/
instance instSeminormedAddGroup [SeminormedAddGroup E] : SeminormedAddGroup Eᵐᵒᵖ
where
__ := instPseudoMetricSpace
norm x := ‖x.unop‖
dist_eq _ _ := dist_eq_norm _ _
