nonempty_diffeomorph_sphere_three

Mathlib.Geometry.Manifold.PoincareConjecture

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

Lean4

/-- The 3-dimensional smooth Poincaré conjecture (proven by Perelman) -/
axiom nonempty_diffeomorph_sphere_three [T2Space M] [ChartedSpace (ℝ ³) M] [IsManifold (𝓡 3) ∞ M]
    [SimplyConnectedSpace M] [CompactSpace M] : Nonempty (M ≃ₘ⟮𝓡 3, 𝓡 3⟯ 𝕊 ³)

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

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

Разделы

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

Аффилиация

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