IsometryEquiv.map_midpoint
theorem IsometryEquiv.map_midpoint :
∀ {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : MetricSpace PE] [inst_3 : NormedAddTorsor E PE]
[inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MetricSpace PF]
[inst_7 : NormedAddTorsor F PF] (f : PE ≃ᵢ PF) (x y : PE), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
The theorem `IsometryEquiv.map_midpoint` states that for any bijective isometry `f` (a function that preserves distance and has an inverse), given any two points `x` and `y` in a normed add-torsor (a space where you can "add" points and vectors) over a normed add-commutative group (a space where addition is commutative and a norm is defined), the image of the midpoint between `x` and `y` under `f` is the same as the midpoint between the images of `x` and `y` under `f`. In other words, the bijective isometry `f` preserves the property of being a midpoint.
More concisely: For any bijective isometry between normed add-torsors over normed add-commutative groups, the image of the midpoint between two points is the midpoint of their images.
|
IsometryEquiv.midpoint_fixed
theorem IsometryEquiv.midpoint_fixed :
∀ {E : Type u_1} {PE : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MetricSpace PE]
[inst_3 : NormedAddTorsor E PE] {x y : PE} (e : PE ≃ᵢ PE),
e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y
This theorem states that if you have an isometric self-homeomorphism, essentially a continuous transformation that preserves distance, in a normed vector space over the real numbers, and this transformation fixes two points `x` and `y` (meaning the transformation doesn't change their location), then it also fixes the midpoint of the line segment between `x` and `y`. This theorem is a lemma, or helping theorem, for a more general theorem known as the Mazur-Ulam theorem.
More concisely: If `f : X → X` is an isometric self-homeomorphism of a real normed vector space `X`, and `x, y ∈ X` are such that `f(x) = x` and `f(y) = y`, then `f` fixes the midpoint of the segment `[x, y]`.
|