Skip to content

fix(Geometry/Manifold): restore the Hausdorff hypothesis in NonemptyDiffeomorphSphere #43606

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Deicyde wants to merge 9 commits into
base: master
Choose a base branch
from
Open

fix(Geometry/Manifold): restore the Hausdorff hypothesis in NonemptyDiffeomorphSphere #43606

Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
1a56011
fix(Geometry/Manifold): restore the Hausdorff hypothesis in `Nonempty…
Deicyde Sep 9, 2026
0af4b69
Update PoincareConjecture.lean
Deicyde Sep 9, 2026
642671f
fix: state the Hausdorff hypothesis inside the quantifier
Deicyde Sep 9, 2026
aa1d38b
Merge branch 'master' into poincare-t2space
Deicyde Sep 9, 2026
1de1ab3
move the Hausdorff hypothesis into the signature of `NonemptyDiffeomo…
Deicyde Sep 9, 2026
e9ace00
Merge branch 'master' into poincare-t2space
Deicyde Sep 9, 2026
2947c75
Remove comment
Deicyde Sep 9, 2026
05f186d
Fix whitespace
Deicyde Sep 9, 2026
915b9d6
Merge branch 'master' into poincare-t2space
Deicyde Sep 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Mathlib/Geometry/Manifold/PoincareConjecture.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ open ContinuousMap
/-- 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). -/
def ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere (n : ℕ) : Prop :=
@[nolint unusedArguments]
def ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere [T2Space M] (n : ℕ) : Prop :=
∀ (_ : ChartedSpace ℝⁿ M) (_ : IsManifold (𝓡 n) ∞ M),
M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₘ⟮𝓡 n, 𝓡 n⟯ 𝕊ⁿ)
Loading