Commit 2025-08-22 14:10 ed3702c1

View on Github →

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

Estimated changes

Modified Mathlib/Order/Filter/Ker.lean

added theorem Filter.ker_pi

added theorem Filter.ker_prod

Modified Mathlib/Topology/AlexandrovDiscrete.lean

added theorem alexandrovDiscrete_iff_isClosed

added theorem alexandrovDiscrete_iff_nhds

modified theorem isClosed_sUnion

Modified Mathlib/Topology/NhdsKer.lean

added theorem nhdsKer_biUnion

added theorem nhdsKer_pair

added theorem nhdsKer_pi

added theorem nhdsKer_prod

added theorem nhdsKer_singleton_pi