Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-01 12:08 aa673157

View on Github →

chore(order/filter/bases): generalize has_basis.restrict (#3645) The old lemma is renamed to filter.has_basis.restrict_subset

Estimated changes

modified theorem filter.has_basis.restrict