-
Notifications
You must be signed in to change notification settings - Fork 47
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
Alexandroff-Hausdorff Theorem and the Cantor Space #834
Conversation
7887bb2
to
0e0cd16
Compare
76051f2
to
62027c7
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is essentially a pass of linting.
It must be rebased on master to update the changelog.
This should be easy because the unreleased changelog file is empty right now.
Just need to copy-paste the following in the Added
section:
- in file `cantor.v`,
+ new definitions `cantor_space`, `cantor_like`, `pointedDiscrete`, and
`tree_of`.
+ new lemmas `cantor_space_compact`, `cantor_space_hausdorff`,
`cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`,
`tree_map_props`, `homeomorphism_cantor_like`, and
`cantor_like_finite_prod`.
+ new theorem `cantor_surj`.
- in file `topology.v`,
+ new lemmas `perfect_set2`, and `ent_closure`.
I tried to simplify the scripts by naming hypothesis, clarifying the flow
locally and shortening when reasonable (btw, I heard that the rule for
?
is to use it to gain space only when the subgoal is closed on the same line
?
are introduced, otherwise variables'd better be named).
It looks like ent_closure
was duplicated, that's why it appears as deleted in the diff,
you may want to double-check.
proof going through unused proofs linting metric implies countable uniformity fixing changelog linting proving sups preserve countable ent proof going through unused proofs linting metric implies countable uniformity linting metric for products linting fixing docs moving cantor stuff to topology discrete metric building clopen set trying for xneqy trying to build inside out cluster set1 proving compact countable basis lots of helpful lemmas simplify proof with near_covering proof cleanup adding perfect stuff buildling tree for homeomorphism cantor_like space homeomorphism done starting cleanup deleting old stuff working through finitely branching trees proving sups preserve countable ent proof going through unused proofs linting metric implies countable uniformity fixing changelog linting proving sups preserve countable ent proof going through unused proofs linting metric implies countable uniformity linting metric for products linting fixing docs lots of helpful lemmas simplify proof with near_covering proof cleanup adding perfect stuff buildling tree for homeomorphism cantor_like space homeomorphism done starting cleanup working through finitely branching trees middle thirds refining tree indexed refinement of trees trying to define tree levels branch sets cauchy branches need finite upper bounds fixing target target now works correctly surjectivity done working on prefixes just tree prefix remaining alexandroff hausdorff is done (but terrible) whitespace
Co-authored-by: affeldt-aist <[email protected]>
2b3a37b
to
d94f5d2
Compare
d94f5d2
to
85f0990
Compare
-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
-- Co-authored-by: zstone1 <[email protected]>
Motivation for this change
The Alexandroff-Hausdorff Theorem says "every compact metric space is the continuous image of the cantor space." This is, as far as I know, the first formalization of this result. The proof is one of two classical approaches, and goes via finitely branching trees. (The other using compact metric spaces embeding into
[0,1]^nat
.) This makes a fairly dramatic refactoring of the classical textbook proof. Turns out the two main lemmasshare a lot of content. Refactoring this things went from ~1000 lines to ~ 500 lines.
There are still some fairly technical details that aren't essential to grasp the whole idea technique. But the hopefully the outline is clear.
This is the culmination of several other pieces of work, most notably the "countable uniformity" stuff.
compact -> complete
. Cantor misc #893Things done/to do
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
)Automatic note to reviewers
Read this Checklist and put a milestone if possible.