mathlib3

94fd004d - feat(order/minimal): Subset of minimal/maximal elements (#11268)

feat(order/minimal): Subset of minimal/maximal elements (#11268) This defines `minimals r s`/`maximals r s` the minimal/maximal elements of `s` with respect to relation `r`.