Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.has_basis_infi

Modification history

2022-06-11 11:06
src/order/filter/bases.lean
feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118) …
Modified filter.has_basis_infiView on Github →
2022-02-14 06:18
src/order/filter/bases.lean
feat(order/filter/bases): basis of infimum of filters (#11855)
Added filter.has_basis_infiView on Github →