Def Filter.curry

Modification history

2024-10-09 04:43

Mathlib/Order/Filter/Curry.lean

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

Modified Filter.curry View on Github →

2024-05-26 16:34

Mathlib/Order/Filter/Curry.lean

chore: redefine Filter.curry in terms of Filter.bind (#13044) …

Modified Filter.curry View on Github →

2023-01-23 13:01

Mathlib/Order/Filter/Curry.lean

Feat: port Order.Filter.Curry (#1773)

Added Filter.curry View on Github →