Point reflection in a point as an isometric homeomorphism
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.
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.
Tags
point reflection, isometric
theorem
equiv.point_reflection_fixed_iff_of_module
(R : Type u_1)
{E : Type u_2}
[ring R]
[invertible 2]
[add_comm_group E]
[module R E]
{x y : E} :
⇑(equiv.point_reflection x) y = y ↔ y = x
Point reflection in x as an isometric homeomorphism.
Equations
- isometric.point_reflection x = (isometric.neg E).trans (isometric.add_left (x + x))
theorem
isometric.point_reflection_apply
{E : Type u_2}
[normed_group E]
(x y : E) :
⇑(isometric.point_reflection x) y = x + x - y
@[simp]
@[simp]
theorem
isometric.point_reflection_self
{E : Type u_2}
[normed_group E]
(x : E) :
⇑(isometric.point_reflection x) x = x
@[simp]
@[simp]
theorem
isometric.point_reflection_dist_fixed
{E : Type u_2}
[normed_group E]
(x y : E) :
has_dist.dist (⇑(isometric.point_reflection x) y) x = has_dist.dist y x
theorem
isometric.point_reflection_dist_self'
{E : Type u_2}
[normed_group E]
(x y : E) :
has_dist.dist (⇑(isometric.point_reflection x) y) y = has_dist.dist (x + x) (y + y)
@[simp]
theorem
isometric.point_reflection_midpoint_left
(R : Type u_1)
{E : Type u_2}
[ring R]
[invertible 2]
[normed_group E]
[module R E]
(x y : E) :
⇑(isometric.point_reflection (midpoint R x y)) x = y
@[simp]
theorem
isometric.point_reflection_midpoint_right
(R : Type u_1)
{E : Type u_2}
[ring R]
[invertible 2]
[normed_group E]
[module R E]
(x y : E) :
⇑(isometric.point_reflection (midpoint R x y)) y = x
theorem
isometric.point_reflection_fixed_iff
(R : Type u_1)
{E : Type u_2}
[ring R]
[invertible 2]
[normed_group E]
[module R E]
{x y : E} :
⇑(isometric.point_reflection x) y = y ↔ y = x
theorem
isometric.point_reflection_dist_self
(R : Type u_1)
{E : Type u_2}
[normed_field R]
[normed_group E]
[normed_space R E]
(x y : E) :
has_dist.dist (⇑(isometric.point_reflection x) y) y = ∥2∥ * has_dist.dist x y
theorem
isometric.point_reflection_dist_self_real
{E : Type u_2}
[normed_group E]
[normed_space ℝ E]
(x y : E) :
has_dist.dist (⇑(isometric.point_reflection x) y) y = 2 * has_dist.dist x y