Skip to content

feat: prove T604, cardinality at most 饾敔 implies density at most 饾敔 - #1343

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

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

Conversation

@kisonecat

Copy link
Copy Markdown

Adds T604: a space of cardinality at most 饾敔 has density at most 饾敔.

The whole space is dense in itself and has cardinality at most 饾敔 by hypothesis.

Closes #1035.

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.

T604: Cardinality $\leq\mathfrak c$ (P163) => Density $\leq\mathfrak c$ (P209)

1 participant