Skip to content

Manifold with boundary and related properties (part 2)#1752

Open
prabau wants to merge 2 commits intomainfrom
manif-bdry2
Open

Manifold with boundary and related properties (part 2)#1752
prabau wants to merge 2 commits intomainfrom
manif-bdry2

Conversation

@prabau
Copy link
Copy Markdown
Collaborator

@prabau prabau commented Apr 21, 2026

Part 2 of changes for #1736. (Part 1 was #1744)

Updates most theorems with P122 (locally Euclidean) to use P235 (locally a Euclidean half-space).

I did not update the two theorems below, but I think they should also be true for manifolds with boundary. Hope someone with more background in this area can update them in a separate PR.

  • (T461) n-manifold => embeddable into Euclidean space
  • (T685) n-manifold + compact + multiple points => not contractible

Part 3 will updates traits for various spaces.

@prabau prabau added the theorem label Apr 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant