Theorem Filter.ker_prod

Modification history

2025-08-22 14:10
Mathlib/Order/Filter/Ker.lean
feat: Finite product of Alexandrov-discrete spaces is Alexandrov-discrete (#27018)
Added Filter.ker_prodView on Github →