Skip to content

T553 update: hereditarily connected => locally contractible#1729

Merged
felixpernegger merged 2 commits intomainfrom
heredconn-loccontract
Apr 12, 2026
Merged

T553 update: hereditarily connected => locally contractible#1729
felixpernegger merged 2 commits intomainfrom
heredconn-loccontract

Conversation

@prabau
Copy link
Copy Markdown
Collaborator

@prabau prabau commented Apr 10, 2026

  • old T553: hereditarily connected => locally path connected
  • new T553: hereditarily connected => locally contractible

This allows to derive that 6 more spaces are locally contractible:
https://topology.pi-base.org/spaces?q=Hereditarily+connected%2B%3FLocally+contractible

Also remove an asserted trait that can now be derived.

@prabau prabau added the theorem label Apr 10, 2026
@yhx-12243
Copy link
Copy Markdown
Collaborator

yhx-12243 commented Apr 10, 2026

As well as T316 (can be removed due to T848)

@prabau prabau marked this pull request as draft April 10, 2026 20:17
@prabau prabau marked this pull request as ready for review April 11, 2026 04:12
@prabau prabau requested review from felixpernegger and yhx-12243 and removed request for yhx-12243 April 11, 2026 04:12
Copy link
Copy Markdown
Collaborator

@felixpernegger felixpernegger left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nice

@felixpernegger felixpernegger merged commit d182b6e into main Apr 12, 2026
1 check passed
@felixpernegger felixpernegger deleted the heredconn-loccontract branch April 12, 2026 00:23
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.

3 participants