English
From a SeminormedGroup and a separation condition h, NormedGroup.ofSeparation yields a NormedGroup structure with dist and eq_of_dist_eq_zero derived from h.
Русский
Из SeminormedGroup и условия разделения h получается структура NormedGroup через NormedGroup.ofSeparation, где dist и eq_of_dist_eq_zero задаются через h.
LaTeX
$$$\text{NormedGroup.ofSeparation } h$ yields a NormedGroup with dist_eq := ‹SeminormedGroup E›.dist_eq and eq_of_dist_eq_zero := h.$$
Lean4
/-- Construct a `NormedCommGroup` from a `SeminormedCommGroup` satisfying
`∀ x, ‖x‖ = 0 → x = 1`. This avoids having to go back to the `(Pseudo)MetricSpace` level when
declaring a `NormedCommGroup` instance as a special case of a more general `SeminormedCommGroup`
instance. -/
@[to_additive /-- Construct a `NormedAddCommGroup` from a
`SeminormedAddCommGroup` satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the
`(Pseudo)MetricSpace` level when declaring a `NormedAddCommGroup` instance as a special case
of a more general `SeminormedAddCommGroup` instance. -/
]
abbrev ofSeparation [SeminormedCommGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) : NormedCommGroup E :=
{ ‹SeminormedCommGroup E›, NormedGroup.ofSeparation h with }
-- See note [reducible non-instances]
