mathlib3

cd7b23d1 - feat(topology/subset_properties): `locally_compact_space` instance for `Π` types (#15707)

feat(topology/subset_properties): `locally_compact_space` instance for `Π` types (#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>