Theorem RestrictedProduct.isOpen_forall_imp_mem_of_principal

Modification history

2025-03-17 22:05
Mathlib/Topology/Algebra/RestrictedProduct.lean
feat: restricted products and their topology (#20021)
Added RestrictedProduct.isOpen_forall_imp_mem_of_principalView on Github →