Theorem filter.is_countably_generated_seq
Modification history
2022-08-30 13:54
src/order/filter/bases.lean
chore(analysis, measure_theory): Fix lint (#16216) …
Modified filter.is_countably_generated_seqView on Github →2022-07-26 11:31
src/order/filter/bases.lean
feat(order/filter/*): `filter.pi` is countably generated (#15632) …
Modified filter.is_countably_generated_seqView on Github →2021-10-23 17:11
src/order/filter/bases.lean
refactor(order/filter/bases): turn `is_countably_generated` into a class (#9838) …
Modified filter.is_countably_generated_seqView on Github →