mathlib3

f384f5d1 - refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (#17361)

refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (#17361) Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>