Commit 2024-09-11 03:53 00efa9fd

View on Github →

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

Estimated changes

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.comap_prodMap_prod

added theorem Filter.prod_eq_inf