Skip to content

feat: prove T297, countably many continuous self-maps implies countable - #1339

Open
kisonecat wants to merge 1 commit into
felixpernegger:masterfrom
kisonecat:formalize-T297
Open

kisonecat wants to merge 1 commit into
felixpernegger:masterfrom
kisonecat:formalize-T297

Conversation

@kisonecat

Copy link
Copy Markdown

Adds T297: a space with countably many continuous self-maps is countable.

Constant maps are continuous, and distinct points give distinct constant maps, so X injects
into C(X, X). Recovering the point from the constant map needs a point to evaluate at, so
the empty space is handled separately — where the conclusion is immediate.

This is the proof π-base records: each constant map is a continuous map.

Closes #551.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

T297: Countably-many continuous self-maps (P138) => Countable (P57)

1 participant