Given a normed_group E and x : E, we define isometric.point_reflection x to be
the point reflection in x interpreted as an isometric homeomorphism.
x : E
Point reflection is defined as an equiv.perm in data.equiv.mul_add. In this file
we restate results about equiv.point_reflection for an isometric.point_reflection, and
add a few results about dist.
point reflection, isometric
Point reflection in x as an isometric homeomorphism.