eq_reflection_of_eq_subspace — Mathlib

English

If two affine subspaces s and s' are equal, then reflecting any point p across either subspace yields the same result.

Русский

Если два аффинных подпространства s и s' равны, то отражение любой точки p через каждое из них даёт одинаковый результат.

LaTeX

$$$$\text{If } s = s' \text{, then } \mathrm{reflection}_s(p) = \mathrm{reflection}_{s'}(p) \text{ for all } p.$$$$

Lean4

theorem eq_reflection_of_eq_subspace {s s' : AffineSubspace ℝ P} [Nonempty s] [Nonempty s']
    [s.direction.HasOrthogonalProjection] [s'.direction.HasOrthogonalProjection] (h : s = s') (p : P) :
    (reflection s p : P) = (reflection s' p : P) := by
  subst h
  rfl

Похожие утверждения