Lean4
/-- Reflection in an affine subspace, which is expected to be nonempty
and complete. The word "reflection" is sometimes understood to mean
specifically reflection in a codimension-one subspace, and sometimes
more generally to cover operations such as reflection in a point. The
definition here, of reflection in an affine subspace, is a more
general sense of the word that includes both those common cases. -/
def reflection (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] : P ≃ᵃⁱ[ℝ] P :=
AffineIsometryEquiv.mk' (fun p => (↑(orthogonalProjection s p) -ᵥ p) +ᵥ (orthogonalProjection s p : P))
s.direction.reflection (↑(Classical.arbitrary s))
(by
intro p
let v := p -ᵥ ↑(Classical.arbitrary s)
let a : V := s.direction.orthogonalProjection v
let b : P := ↑(Classical.arbitrary s)
have key : ((a +ᵥ b) -ᵥ (v +ᵥ b)) +ᵥ (a +ᵥ b) = (a + a - v) +ᵥ (b -ᵥ b) +ᵥ b :=
by
rw [← add_vadd, vsub_vadd_eq_vsub_sub, vsub_vadd, vadd_vsub]
congr 1
abel
dsimp only
rwa [Submodule.reflection_apply, (vsub_vadd p b).symm, ContinuousAffineMap.map_vadd,
orthogonalProjection_contLinear, vadd_vsub, orthogonalProjection_mem_subspace_eq_self, two_smul])
