Theorems · Inductive type · functional analysis

NormedAddTorsor

(V : outParam (Type u_1)) → (P : Type u_2) → [SeminormedAddCommGroup V] → [PseudoMetricSpace P] → Type (max u_1 u_2)

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

Cited by

1,325 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SeminormedAddCommGroupPseudoMetricSpace