mathlib3
975f41a4 - feat(order): closure operators (#5524)

Commit
5 years ago
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.
Author
Parents
Loading