Commit 2023-01-25 06:25 2987594a
View on Github →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.