mathlib
178a3265 - chore(topology/category/Top/limits): split file (#18871)

Commit
2 years ago
chore(topology/category/Top/limits): split file (#18871) Per https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233487.20last.20minute.20split.3F This file is already being ported at https://github.com/leanprover-community/mathlib4/pull/3487, but: * it's not going so well right now * it is going well up to the point of the proposed new `limits/basic.lean` * that is sufficient to port the files needed for Copenhagen Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading