[Merged by Bors] - feat(Topology): some lemmas about continuity of maps out of one point compactifications#13355
[Merged by Bors] - feat(Topology): some lemmas about continuity of maps out of one point compactifications#13355dagurtomas wants to merge 12 commits intomasterfrom
Conversation
…point compactifications
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
|
Can you add a More generally, is there a universal property I think (I don't know in which category), sooner or later we will want that. |
|
The universal property should be something like That is, there should probably be something like |
|
I added some constructors which take a continuous map and a "limit value" and produce a continuous map from |
PR summary 9dfbf9a24eImport changesNo significant changes to the import graph
|
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
|
Thanks! |
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by faenuccio. |
|
Thanks! bors merge |
… compactifications (#13355) We prove that a map out of the one point compactification of `X` is continuous if and only if its restriction to `X` satisfies the two properties 1) is continuous 2) is continuous "at infinity", namely that it tends to the value at infinity for the `coclosedCompact` filter on `X` We deduce that continuous functions out of the one point compactification of the natural numbers correspond to convergent sequences. We also prove that the one point compactification of a discrete space is totally separated. Co-authored-by: Jireh Loreaux Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>
|
Pull request successfully merged into master. Build succeeded: |
… compactifications (#13355) We prove that a map out of the one point compactification of `X` is continuous if and only if its restriction to `X` satisfies the two properties 1) is continuous 2) is continuous "at infinity", namely that it tends to the value at infinity for the `coclosedCompact` filter on `X` We deduce that continuous functions out of the one point compactification of the natural numbers correspond to convergent sequences. We also prove that the one point compactification of a discrete space is totally separated. Co-authored-by: Jireh Loreaux Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>
We prove that a map out of the one point compactification of
Xis continuous if and only if its restriction toXsatisfies the two propertiescoclosedCompactfilter onXWe deduce that continuous functions out of the one point compactification of the natural numbers correspond to convergent sequences.
We also prove that the one point compactification of a discrete space is totally separated.
Co-authored-by: Jireh Loreaux
This is all in preparation for the definition of
ℕ ∪ {∞}as a light profinite set, which is important in light condensed mathematics.