Commit 2022-02-24 11:57 b8b1b578View on Github →
chore(geometry/euclidean): split repetitive proof (#12209)
This PR is part of the subobject refactor #11545, fixing a timeout caused by some expensive defeq checks.
I introduce a new definition
simplex.orthogonal_projection_span s := orthogonal_projection (affine_span ℝ (set.range s.points)), and extract a couple of its properties from (repetitive) parts of proofs in
eq_or_eq_reflection_of_dist_eq. This makes the latter proof noticeably faster, especially after commit #11750.