Arzela-Ascoli #397
Closed
Arzela-Ascoli #397
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Adding dependent pair technique for convergence, and unif -> ptws
|
This was successfully broken into smaller changes and dramatically improved. All those changes have been merged, so this is now redundant. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A proof of Ascoli's theorem. That is, given a topological space X, and a hausdorff uniform space Y, pointwise compact images + equicontinuous -> compact in the topology of compact convergence. The converse is true when X is locally compact hausdorff, which I also prove. Additionally, this diff splits out all the of the results about function space topologies into a separate file to try to manage the size of topology.v.
I had to prove a bunch of other useful stuff along the way, such as products of hausdorff are hausdorff. I follow more-or-less the textbook proof from munkeres, making adjustments as necessary to deal with filters and and uniform spaces instead of open sets and metric spaces. Thankfully tychonoff is already done.
I end up having to do a lot of work that feels like it should be factored into a
nearnotation. In particular, I have a lot of proof lines just splitting entourages and proving their rather boring relationships. I'm wondering if there's a better approach, using the filter of{E, split E, split (split E) ...} U {E^-1, (split E) ^-1,...}.This depends on #311 heavily, So that has to be merged first. But I figured I would put it up for review in the meanwhile.