English
Let E be a sem normed group and h: ∀ x, ∥x∥ = 0 → x = 1. Then there is a NormedGroup structure on E whose distance agrees with the seminormed distance and whose zero-distance condition follows from h.
Русский
Пусть E — полунормированная группа и дано условие разделимости h: ∥x∥ = 0 → x = 1. Тогда на E существует структура NormedGroup, у которой расстояние согласуется с расстоянием полугруппы по норме, и нулевое различие даёт единицу.
LaTeX
$$$\exists \text{NormedGroup } E \text{ such that dist(x,y)=∥x y^{-1}∥ and ∥x∥ = dist(x,1)$ (via h).$$
Lean4
/-- Construct a `NormedGroup` from a `SeminormedGroup` satisfying `∀ x, ‖x‖ = 0 → x = 1`. This
avoids having to go back to the `(Pseudo)MetricSpace` level when declaring a `NormedGroup`
instance as a special case of a more general `SeminormedGroup` instance. -/
@[to_additive /-- Construct a `NormedAddGroup` from a `SeminormedAddGroup`
satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the `(Pseudo)MetricSpace`
level when declaring a `NormedAddGroup` instance as a special case of a more general
`SeminormedAddGroup` instance. -/
]
abbrev ofSeparation [SeminormedGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) : NormedGroup E
where
dist_eq := ‹SeminormedGroup E›.dist_eq
toMetricSpace :=
{ eq_of_dist_eq_zero := fun hxy => div_eq_one.1 <| h _ <| (‹SeminormedGroup E›.dist_eq _ _).symm.trans hxy }
-- See note [reducible non-instances]
