nonempty_homeomorph_sphere_three

Mathlib.Geometry.Manifold.PoincareConjecture

URI: https://scilib.ai/kg/mathlib#SimplyConnectedSpace.nonempty_homeomorph_sphere_three

Lean4

/-- The 3-dimensional topological Poincaré conjecture (proven by Perelman) -/
axiom nonempty_homeomorph_sphere_three [T2Space M] [ChartedSpace (ℝ ³) M] [SimplyConnectedSpace M] [CompactSpace M] :
    Nonempty (M ≃ₜ 𝕊 ³)

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

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

Разделы

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

Аффилиация

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