Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-17 02:59 1b1b626a

View on Github →

chore(topology/sequences): use filter bases, minor fixes (#2001)

Estimated changes

modified def is_seq_closed