filter): add two lemmas (#9956)

Commit

4 years ago

feat(algebra/order/group|order/filter): add two lemmas (#9956) * Also open `function` namespace in `order.filter.basic` * From the sphere eversion project

Author

fpvandoorn

Parents

41df5b35

mathlib d2b12217 - feat(algebra/order/group|order/filter): add two lemmas (#9956)

mathlib
d2b12217 - feat(algebra/order/group|order/filter): add two lemmas (#9956)