Theorems · Definition · functional analysis

NormedCommGroup.ofSeparation

{E : Type u_5} → [inst : SeminormedCommGroup E] → (∀ (x : E), ‖x‖ = 0 → x = 1) → NormedCommGroup E

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.

Defined in

Mathlib.Analysis.Normed.Group.Defs

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedCommGroup