mathlib

dde670c9 - chore(topology/constructions): pi.single is continuous (#18412)

chore(topology/constructions): pi.single is continuous (#18412) Forward-ported in https://github.com/leanprover-community/mathlib4/pull/2176. I found this convenient for proving continuity of `![r, 0, 0, 0]` via `convert`.