Commit 2023-12-15 13:12 c8c1c7a6

View on Github →

feat(Filter/Basic): define Filter.copy (#9056)

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.copy_eq

added theorem Filter.mem_copy