nonempty_homeomorph_sphere

Mathlib.Geometry.Manifold.PoincareConjecture

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere

Lean4

/-- The generalized topological Poincaré conjecture.
- For n = 2 it follows from the classification of surfaces.
- For n ≥ 5 it was proven by Stephen Smale in 1961 assuming M admits a smooth structure;
  Newman (1966) and Connell (1967) proved it without the condition.
- For n = 4 it was proven by Michael Freedman in 1982.
- For n = 3 it was proven by Grigori Perelman in 2003. -/
axiom nonempty_homeomorph_sphere [T2Space M] (n : ℕ) [ChartedSpace (ℝ ⁿ) M] : (M ≃ₕ 𝕊 ⁿ) → Nonempty (M ≃ₜ 𝕊 ⁿ)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru