exists_open_nonempty_homeomorph_isEmpty_diffeomorph_euclideanSpace_four

Mathlib.Geometry.Manifold.PoincareConjecture

URI: https://scilib.ai/kg/mathlib#exists_open_nonempty_homeomorph_isEmpty_diffeomorph_euclideanSpace_four

Lean4

/-- The existence of a small exotic ℝ⁴, i.e. an open subset of ℝ⁴ that is homeomorphic but
not diffeomorphic to ℝ⁴. See https://en.wikipedia.org/wiki/Exotic_R4. -/
axiom exists_open_nonempty_homeomorph_isEmpty_diffeomorph_euclideanSpace_four :
    ∃ M : TopologicalSpace.Opens ℝ ⁴, Nonempty (M ≃ₜ ℝ ⁴) ∧ IsEmpty (M ≃ₘ⟮𝓡 4, 𝓡 4⟯ ℝ ⁴)

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

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

Разделы

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

Аффилиация

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