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 : ℕ) : Prop

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.