Theorem DiscreteTopology.isDiscrete

Modification history

2025-11-25 20:26

Mathlib/Topology/Constructions.lean

feat(Topology/Constructions): `IsDiscrete` predicate on sets (#30349) …

Added DiscreteTopology.isDiscrete View on Github →