converse to docs#set.countable_univ

Stream: Is there code for X?

[Felix Weilacher]

I would like to prove countable α from (univ : set α).countable.

It follows from docs#set.countable.to_subtype, docs#countable.of_equiv, and docs#equiv.set.univ but it also seems like something we might already have.

[Felix Weilacher]

docs#set.countable_univ since apparently the link doesn't work in the topic

[Yaël Dillies]

To be honest, I would have expected set.countable_univ : (univ : set α).countable ↔ countable α.