Torsors of additive normed group actions. #
This file defines torsors of additive normed group actions, with a metric space structure. The motivating case is Euclidean affine spaces.
- vadd : V → P → P
- vsub : P → P → V
- Nonempty : Nonempty P
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).
Instances
Shortcut instance to help typeclass inference out.
A SeminormedAddCommGroup
is a NormedAddTorsor
over itself.
A nonempty affine subspace of a NormedAddTorsor
is itself a NormedAddTorsor
.
The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have V
as an explicit argument; otherwise
rw dist_eq_norm_vsub
sometimes doesn't work.
The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have V
as an explicit argument; otherwise
rw dist_eq_norm_vsub'
sometimes doesn't work.
Isometry between the tangent space V
of a (semi)normed add torsor P
and P
given by
addition/subtraction of x : P
.
Instances For
Isometry between the tangent space V
of a (semi)normed add torsor P
and P
given by
subtraction from x : P
.
Instances For
The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on V
to define a MetricSpace P
.
Instances For
The distance defines a metric space structure on the torsor. This
is not an instance because it depends on V
to define a MetricSpace P
.