discrete topology type alias

Stream: Is there code for X?

[Johan Commelin]

Do we have a type alias that endows a topological space with the discrete topology?

[Patrick Massot]

No.

[Adam Topaz]

@Johan Commelin (forget Profinite).obj

[Adam Topaz]

(I assume this is for the stone Cech thing, in which case you could just use ultrafilter instead of stone_cech)

[Johan Commelin]

That turns X into a Type, but it still doesn't get the discrete topology that way, right?

[Adam Topaz]

We have docs#Top.discrete too

[Johan Commelin]

Yes, I think that's useful.

[Adam Topaz]

If X : Profinite then ultrafilter X is the stone Cech compactififcation of the discrete set

[Johan Commelin]

Aha, and it comes equipped with all the topology stuff etc?

[Johan Commelin]

Let me try

[Adam Topaz]

I think it might be missing a totally disconnected instance, but all the other instances should be there