Commit 2023-01-23 13:01 cdcd203e

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Curry.lean

added theorem Filter.Tendsto.curry

added def Filter.curry

added theorem Filter.curry_le_prod

added theorem Filter.eventually_curry_iff