Commit 2024-01-12 06:00 d91d6797
View on Github →feat(Cardinal): #(α ≃ β) and #(α ↪ β) in the infinite case (#9646)
Main results:
- If two types have the same infinite cardinality, then there are as many Equivs between them as there are functions.
- If B has infinite cardinality no less than #A, then there are as many embeddings from A into B as there are functions.
- If A has infinite cardinality no less than #B, then there are as many surjective functions from A to B as there are functions.