# Commit 2022-10-05 09:32 a4d24238

View on Github →feat(geometry/euclidean/basic): bundled spheres (#16184)
Define a bundled `sphere`

structure, for various uses in Euclidean
geometry where it's convenient to pass around `center`

and `radius`

together.
Some basic API is set up for this structure, including `sphere`

versions of a few existing lemmas that could naturally be expressed in
that way. The construction of `circumcenter`

and `circumradius`

is
also changed to pass around a `sphere`

instead of using `P × ℝ`

. It
is likely that other existing lemmas can usefully have bundled sphere
versions added in followups. Certainly there are plenty of other
definitions and results about spheres that can usefully be built up on
top of this basic API.
Notes:

- As with
`cospherical`

, the definition and some of the most basic lemmas don't actually need anything more than the metric space structure.`sphere`

is defined alongside`cospherical`

, but it would also be reasonable to define both in some metric space file. In that case, the name of`sphere`

would need to change to avoid conflicts with the existing`metric.sphere`

(which is part of a family of unbundled definitions with`metric.ball`

and`metric.closed_ball`

, so should probably remain as-is). - The definition doesn't include any non-degeneracy conditions, so
avoiding the need for users to prove such conditions when
constructing a
`sphere`

for a lemma that doesn't need them. Note that the base case for the induction constructing the circumsphere uses a radius of zero. - I haven't forgotten the discussion in #4088 of simplifying the proof
of
`eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two`

using bundled spheres, a definition of the radical subspace and a proof that a one-dimensional sphere has at most two points (so ending up proving the unbundled lemma using the bundled one rather than vice versa), but I think quite a lot more API about power of a point and radical subspaces would still need adding before that could be done.