Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.mem_prod_self_iff

Modification history

2022-07-26 12:57
src/order/filter/bases.lean
feat(order/filter/bases): lemmas about bases of product filters (#15630) …
Modified filter.mem_prod_self_iffView on Github →
2022-01-11 13:55
src/order/filter/bases.lean
refactor(data/set/prod): add notation class for set-like product (#11300) …
Modified filter.mem_prod_self_iffView on Github →
2020-08-14 15:47
src/order/filter/bases.lean
chore(*): use notation for `filter.prod` (#3768) …
Added filter.mem_prod_self_iffView on Github →