Skip to content
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.

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

Cantor Space Theory: zero dimensional and totally disconnected #886

Merged
merged 4 commits into from
Apr 13, 2023

Conversation

zstone1
Copy link
Contributor

@zstone1 zstone1 commented Mar 28, 2023

Motivation for this change

In continuing to break apart #627 into reviewable chunks, we introduce some basics about zero_dimensional and totally disconnected spaces. That is, spaces where points are separable by clopen sets. For completeness here, I'm also included "totally disconnected" spaces, that is spaces whose only connected components are singletons. These notions respect products, which is the main thing we actually need. A few additional lemmas are also proven to build out the theory a bit.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    (do not edit former entries, only append new ones, be careful:
    merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@zstone1 zstone1 added enhancement ✨ This issue/PR is about adding new features enhancing the library TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. labels Mar 28, 2023
@affeldt-aist affeldt-aist self-requested a review April 12, 2023 06:46
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

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

I found no problem. I just added a commit with minor improvements (a few minor shortenings, removing spurious characters, etc.).

@affeldt-aist affeldt-aist added this to the 0.6.2 milestone Apr 12, 2023
@zstone1 zstone1 merged commit e689a1d into math-comp:master Apr 13, 2023
zstone1 added a commit to zstone1/analysis that referenced this pull request Apr 13, 2023
…comp#886)

* zero dimensional and totally disconnected

* adding docs

* nitpicking

* fixing 8.14 build

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@zstone1 zstone1 mentioned this pull request Apr 13, 2023
3 tasks
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 13, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants