mathlib3

2406dc51 - feat(topology/support): tsupport of product is a subset of tsupport (#15346)