mathlib3

415da222 - chore(topology,measure_theory): generalize a few instances (#9967)

chore(topology,measure_theory): generalize a few instances (#9967) * Prove that `Π i : ι, π i` has second countable topology if `ι` is encodable and each `π i` has second countable topology. * Similarly for `borel_space`. * Preserve old instances about `fintype` because we don't have (and can't have) an instance `fintype ι → encodable ι`.