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.
- to_add_torsor : affine_space V P
- dist_eq_norm' : ∀ (x y : P), has_dist.dist x y = ∥x -ᵥ y∥
A normed_add_torsor V P is a torsor of an additive normed group
action by a normed_group V on points P. We bundle the metric space
structure and require the distance to be the same as results from the
norm (which in fact implies the distance yields a metric space, but
bundling just the distance and using an instance for the metric space
results in type class problems).
Instances
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 defines a metric space structure on the torsor. This
is not an instance because it depends on V to define a metric_space
P.
Equations
- metric_space_of_normed_group_of_add_torsor V P = {to_has_dist := {dist := λ (x y : P), ∥x -ᵥ y∥}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : P), ennreal.of_real ((λ (x y : P), ∥x -ᵥ y∥) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : P), ∥x -ᵥ y∥) _ _ _, uniformity_dist := _}
The map v ↦ v +ᵥ p as an isometric equivalence between V and P.
Equations
- isometric.vadd_const p = {to_equiv := equiv.vadd_const V p, isometry_to_fun := _}
The map p ↦ v +ᵥ p as an isometric automorphism of P.
Equations
- isometric.const_vadd P v = {to_equiv := equiv.const_vadd P v, isometry_to_fun := _}
The map g from V1 to V2 corresponding to a map f from P1
to P2, at a base point p, is an isometry if f is one.