feat(order): closure operators (#5524)
feat(order): closure operators (#5524)

Adds closure operators on a partial order, as in [wikipedia](https://en.wikipedia.org/wiki/Closure_operator#Closure_operators_on_partially_ordered_sets). I made them bundled for no particular reason, I don't mind unbundling.



leanprover-community/mathlib,leanprover-community/mathlib