Commit 2021-10-19 09:31 b961b684

feat(topology/connected): product of connected spaces is a connected space (#9789)

• prove more in the RHS of filter.mem_infi';
• prove that the product of (pre)connected sets is a (pre)connected set;
• prove a similar statement about indexed product set.pi set.univ _;
• add instances for prod.preconnected_space, prod.connected_space, pi.preconnected_space, and pi.connected_space.