mathlib documentation

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] [add_comm_group E] [module R E] {x y : E} :

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) :

@[simp]
theorem isometric.point_reflection_self {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) :

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

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) :