# Statement of the generalized Poincaré conjecture #

https://en.wikipedia.org/wiki/Generalized_Poincar%C3%A9_conjecture

The mathlib notation `≃ₕ`

stands for a homotopy equivalence, `≃ₜ`

stands for a homeomorphism,
and `≃ₘ⟮𝓡 n, 𝓡 n⟯`

stands for a diffeomorphism, where `𝓡 n`

is the `n`

-dimensional Euclidean
space viewed as a model space.

def
ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere
(M : Type u_1)
[TopologicalSpace M]
(n : ℕ)
:

The smooth Poincaré conjecture; true for n = 1, 2, 3, 5, 6, 12, 56, and 61, open for n = 4, and it is conjectured that there are no other n > 4 for which it is true (Conjecture 1.17, https://annals.math.princeton.edu/2017/186-2/p03).

## Equations

- One or more equations did not get rendered due to their size.