Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-14 06:18 77dfac2e

View on Github →

feat(order/filter/bases): basis of infimum of filters (#11855)

Estimated changes

Modified src/order/filter/bases.lean

added theorem filter.has_basis_infi

Modified src/order/filter/pi.lean

added theorem filter.has_basis_pi