CountableSetPresentation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A countable set can be indexed injectively by a closed subset of the natural numbers, so the mark index has its usual discrete Polish structure.