Theorem alexandrovDiscrete_iff_isClosed

Modification history

2025-08-22 14:10

Mathlib/Topology/AlexandrovDiscrete.lean

feat: Finite product of Alexandrov-discrete spaces is Alexandrov-discrete (#27018)

Added alexandrovDiscrete_iff_isClosed View on Github →