Commit 2025-12-11 08:08 8372ba77

View on Github →

refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces (#27378) This PR continues the work from #25578. Original PR: https://github.com/leanprover-community/mathlib4/pull/25578

depends on: #31395

Estimated changes

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/Projection.lean

modified theorem Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection

modified def Affine.Simplex.orthogonalProjectionSpan

modified theorem Affine.Simplex.orthogonalProjectionSpan_congr

modified theorem Affine.Simplex.orthogonalProjectionSpan_eq_point

modified theorem Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev

modified theorem Affine.Simplex.orthogonalProjectionSpan_reindex

modified theorem Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection

modified theorem EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem

modified theorem EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq

modified theorem EuclideanGeometry.dist_orthogonalProjection_eq_infDist

modified theorem EuclideanGeometry.dist_orthogonalProjection_eq_infNndist

modified theorem EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff

modified theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem

modified theorem EuclideanGeometry.dist_reflection

modified theorem EuclideanGeometry.dist_reflection_eq_of_mem

modified theorem EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq

modified theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd

modified theorem EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace

modified theorem EuclideanGeometry.eq_reflection_of_eq_subspace

modified theorem EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq

modified theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjection

deleted theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjectionFn

added def EuclideanGeometry.orthogonalProjection

deleted def EuclideanGeometry.orthogonalProjectionFn

deleted theorem EuclideanGeometry.orthogonalProjectionFn_eq

deleted theorem EuclideanGeometry.orthogonalProjectionFn_mem

deleted theorem EuclideanGeometry.orthogonalProjectionFn_mem_orthogonal

deleted theorem EuclideanGeometry.orthogonalProjectionFn_vsub_mem_direction_orthogonal

added theorem EuclideanGeometry.orthogonalProjection_apply'

added theorem EuclideanGeometry.orthogonalProjection_apply

added theorem EuclideanGeometry.orthogonalProjection_apply_mem

modified theorem EuclideanGeometry.orthogonalProjection_congr

modified theorem EuclideanGeometry.orthogonalProjection_contLinear

modified theorem EuclideanGeometry.orthogonalProjection_eq_iff_mem

modified theorem EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem

modified theorem EuclideanGeometry.orthogonalProjection_eq_self_iff

modified theorem EuclideanGeometry.orthogonalProjection_linear

modified theorem EuclideanGeometry.orthogonalProjection_mem

modified theorem EuclideanGeometry.orthogonalProjection_mem_orthogonal

modified theorem EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self

modified theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection

modified theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le

modified theorem EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq

modified theorem EuclideanGeometry.orthogonalProjection_vadd_eq_self

modified theorem EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection

modified theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction

modified theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal

modified theorem EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection

modified def EuclideanGeometry.reflection

added theorem EuclideanGeometry.reflection_apply'

modified theorem EuclideanGeometry.reflection_apply

added theorem EuclideanGeometry.reflection_apply_of_mem

modified theorem EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq

modified theorem EuclideanGeometry.reflection_eq_self_iff

modified theorem EuclideanGeometry.reflection_involutive

modified theorem EuclideanGeometry.reflection_mem_of_le_of_mem

modified theorem EuclideanGeometry.reflection_orthogonal_vadd

modified theorem EuclideanGeometry.reflection_reflection

modified theorem EuclideanGeometry.reflection_symm

modified theorem EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection

modified theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction

modified theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal