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 : add_torsor 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 seminormed group
action by a semi_normed_group 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 of this typeclass
Instances of other typeclasses for normed_add_torsor
- normed_add_torsor.has_sizeof_inst
A semi_normed_group
is a normed_add_torsor
over itself.
Equations
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
.
Equations
- isometric.vadd_const x = {to_equiv := equiv.vadd_const x, isometry_to_fun := _}
Self-isometry of a (semi)normed add torsor given by addition of a constant vector x
.
Equations
- isometric.const_vadd P x = {to_equiv := equiv.const_vadd P x, isometry_to_fun := _}
Isometry between the tangent space V
of a (semi)normed add torsor P
and P
given by
subtraction from x : P
.
Equations
- isometric.const_vsub x = {to_equiv := equiv.const_vsub x, isometry_to_fun := _}
The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on V
to define a metric_space P
.
Equations
- pseudo_metric_space_of_normed_group_of_add_torsor V P = {to_has_dist := {dist := λ (x y : P), ∥x -ᵥ y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : P), ↑⟨(λ (x y : P), ∥x -ᵥ y∥) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : P), ∥x -ᵥ y∥) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : P), ∥x -ᵥ y∥) _ _ _, cobounded_sets := _}
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_pseudo_metric_space := {to_has_dist := {dist := λ (x y : P), ∥x -ᵥ y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : P), ↑⟨(λ (x y : P), ∥x -ᵥ y∥) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : P), ∥x -ᵥ y∥) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : P), ∥x -ᵥ y∥) _ _ _, cobounded_sets := _}, eq_of_dist_eq_zero := _}