# mathlibdocumentation

analysis.normed_space.point_reflection

# 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] [ E] {x y : E} :
= y y = x

def isometric.point_reflection {E : Type u_2} [normed_group E] :
E → E ≃ᵢ E

Point reflection in x as an isometric homeomorphism.

Equations
theorem isometric.point_reflection_apply {E : Type u_2} [normed_group E] (x y : E) :
= x + x - y

@[simp]
theorem isometric.point_reflection_to_equiv {E : Type u_2} [normed_group E] (x : E) :

@[simp]
theorem isometric.point_reflection_self {E : Type u_2} [normed_group E] (x : E) :
= x

theorem isometric.point_reflection_involutive {E : Type u_2} [normed_group E] (x : E) :

@[simp]
theorem isometric.point_reflection_symm {E : Type u_2} [normed_group E] (x : E) :

@[simp]
theorem isometric.point_reflection_dist_fixed {E : Type u_2} [normed_group E] (x y : E) :
dist y) x = dist y x

theorem isometric.point_reflection_dist_self' {E : Type u_2} [normed_group E] (x y : E) :
dist y) y = 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] [ E] (x y : E) :

@[simp]
theorem isometric.point_reflection_midpoint_right (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [normed_group E] [ E] (x y : E) :

theorem isometric.point_reflection_fixed_iff (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [normed_group E] [ E] {x y : E} :
= y y = x

theorem isometric.point_reflection_dist_self (R : Type u_1) {E : Type u_2} [normed_field R] [normed_group E] [ E] (x y : E) :
dist y) y = 2 * dist x y

theorem isometric.point_reflection_dist_self_real {E : Type u_2} [normed_group E] [ E] (x y : E) :
dist y) y = 2 * dist x y