Theorems · Theorem · geometry

AffineIsometryEquiv.pointReflection_midpoint_left

∀ {V : Type u_2} {P : Type u_10} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : NormedSpace ℝ V] (x y : P),
  (AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) x = y

Defined in

Mathlib.Analysis.Normed.Affine.Isometry

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupPseudoMetricSpaceNormedAddTorsorNormedSpace