mathlib3

ae132cd6 - feat(topology/basic): intersection of a finset-indexed open sets is open (#16075)