Theorems · Theorem · functional analysis

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

If an isometric self-homeomorphism of a normed vector space over ℝ fixes x and y, then it fixes the midpoint of [x, y]. This is a lemma for a more general Mazur-Ulam theorem, see below.

Defined in

Mathlib.Analysis.Normed.Affine.MazurUlam

Cited by

1 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMetricSpaceNormedAddTorsor