mathlib3

2987594a - refactor(topology): move `pcontinuous` etc to a new file (#18288)

refactor(topology): move `pcontinuous` etc to a new file (#18288) Move `pcontinuous` and lemmas about `ptendsto` to a new file. There are some issues with porting `data.pfun` to Lean 4, so this PR makes it possible to port topology without waiting for `pfun`.