`IsDiscrete` predicate

[ADedecker]

In the same way that we have both CompactSpace and IsCompact, one should introduce a predicate IsDiscrete on subsets S : Set X expressing DiscreteTopology S.

Came up in #29743

[loefflerd]

I made a first attempt at this last night (with a lot of help from @j-loreaux); see #30349.

[ADedecker]

Nice! I wasn't sure you were going to go at it right now so I wanted to open the issue, but hopefully it will be closed soon!