Zulip Chat Archive
Stream: general
Topic: cardinality
Dean Young (Feb 24 2023 at 04:17):
I was hoping for some "cardinals" in Lean. I thought that would be a type where isomorphism in Type implies equality in "card", and which is totally ordered. Maybe someone can point me towards the relevant theorem here (about cardinality characterizing isomorphism classes of sets and being a total order).
Junyan Xu (Feb 24 2023 at 04:23):
Junyan Xu (Feb 24 2023 at 04:23):
It's indeed defined as all types (in a universe) modulo nonempty (α ≃ β)
Dean Young (Feb 24 2023 at 07:40):
(deleted)
Johan Commelin (Feb 24 2023 at 07:40):
Lol, but wrong thread?
Dean Young (Feb 24 2023 at 07:41):
Oh right, sorry. Thanks for the cardinality reference.
Last updated: Dec 20 2023 at 11:08 UTC