Skip to content

Remove circular dependency between T851 and T852#1771

Open
prabau wants to merge 3 commits intomainfrom
ord-path-halfline
Open

Remove circular dependency between T851 and T852#1771
prabau wants to merge 3 commits intomainfrom
ord-path-halfline

Conversation

@prabau
Copy link
Copy Markdown
Collaborator

@prabau prabau commented May 6, 2026

Rewrote the argument for T851 (locally orderable => SLSC) to break the dependency on T852.
Also rewrote the argument for T850 (LOTS + path connected => simply connected) used in T851.

And add related new T846 (locally orderable + locally path connected + no isolated points => locally a half-line).

@prabau prabau added the theorem label May 6, 2026
@prabau
Copy link
Copy Markdown
Collaborator Author

prabau commented May 6, 2026

Just realized some traits become redundant with this PR. I'll remove them as well.

@prabau prabau marked this pull request as draft May 6, 2026 07:44
@prabau prabau marked this pull request as ready for review May 7, 2026 05:41
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