Discrete uniformity

Stream: mathlib4

[Antoine Chambert-Loir]

Does it make sense to add a type class that says that a uniformity is the discrete one, analogously to docs#DiscreteTopology?
It would just say : uniformity α = Filter.principal idRel, an assumption that can be found in a few lemmas, docs#discreteTopology_of_discrete_uniformity, and docs#PiNat.metricSpaceOfDiscreteUniformity
That would make it easier to formulate the (trivial) properties of the discrete uniformity (and @María Inés de Frutos Fernández and I need them…)

[Felix Weilacher]

Is this equivalent to the induced topology being the discrete one?

[Antoine Chambert-Loir]

I don't think so: even on an infinite discrete set, you have many distances, and converging uniformly will mean different things for them.

[Felix Weilacher]

Yes, you're right, the induced metric on {1, 1/2, 1/3, ...} induces the discrete topology but not the discrete uniformity.