Structures · Analysis

NormedAddTorsor

A NormedAddTorsor V P is a torsor of an additive seminormed group action by a SeminormedAddCommGroup V on points P. We bundle the pseudometric space structure and require the distance to be the same as results from the norm (which in fact implies the distance yields a pseudometric space, but bundling just the distance and using an instance for the pseudometric space results in type class problems).

Defined in

Mathlib.Analysis.Normed.Group.AddTorsor

Shape

2 explicit arguments · adds dist_eq_norm'