mathlib

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

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`.