mathlib

fc2ed6f8 - feat(logic/denumerable): Any two infinite countable types are equivalent (#17903)

feat(logic/denumerable): Any two infinite countable types are equivalent (#17903) If `α` and `β` are both infinite and countable, then `nonempty (α ≃ β)`. I prove it using the `denumerable` API, but I also provide a lemma to prove it from the `cardinal` one.