Theorem Filter.prod_eq_inf

Modification history

2024-10-09 04:43

Mathlib/Order/Filter/Defs.lean

chore(Filter): move defs to a new file (#17552)

Modified Filter.prod_eq_inf View on Github →

2024-09-11 03:53

Mathlib/Order/Filter/Prod.lean

feat(Filter/Prod): add `comap_prodMap_prod` (#16564)

Added Filter.prod_eq_inf View on Github →