issue !4#30368: `IsDiscrete` predicate

Stream: triage

[Random Issue Bot]

Today I chose issue #30368 for discussion!

IsDiscrete predicate
Created by @Anatole Dedecker (@ADedecker) on 2025-10-09
Labels: t-topology

Is this issue still relevant? Any recent updates? Anyone making progress?

[Andrew Yang]

docs#IsDiscrete is already in mathlib (and somewhat unfortunately in the root namespace)

[Anne Baanen]

Since it exists, should we close this issue then?

[Miyahara Kō]

I think so too.

[Yaël Dillies]

Done

[Anatole Dedecker]

Yes, this is exactly what I had in mind.