Revision #2355 → #3035 · back to history
modifiedn-sphere is a compact topological manifold8c0aaa77bf64
| Field | From #2355 | To #3035 |
|---|
| mathlib.match_kind | exact | — |
| note | The unit sphere in `EuclideanSpace ℝ (Fin (n+1))` is given a `ChartedSpace` instance over `EuclideanSpace ℝ (Fin n)` and is compact via `isCompact_sphere`. | The unit sphere in `EuclideanSpace ℝ (Fin (n+1))` is given a `ChartedSpace` instance over `EuclideanSpace ℝ (Fin n)` and is compact via `isCompact_sphere`; the manifold-with-boundary/boundaryless packaging is spread across several instances. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedSphere in Z^n may be empty18694cf0065c
| Field | From #2355 | To #3035 |
|---|
| anchor.snippet | in Z | a sphere of radius r is nonempty only if |
| note | Mathlib has emptiness lemmas like `sphere_eq_empty_of_subsingleton` and `sphere_eq_empty_of_neg`, but no specific example computing spheres in `ℤⁿ`. | Mathlib has emptiness lemmas like `sphere_eq_empty_of_subsingleton` and `sphere_eq_empty_of_neg`, but no specific example computing spheres in `ℤⁿ` via sums of squares. |
| provenance | ai | ai-moderated |
addedDiameter equals twice the radius254bd5b90ebc
addedSpherical geometry is a form of elliptic geometry265de49d91af