mathlib

6102d771 - feat(group_theory/submonoid/pointwise): pointwise inverse of a submonoid (#10451)

feat(group_theory/submonoid/pointwise): pointwise inverse of a submonoid (#10451) This also adds `order_iso.map_{supr,infi,Sup,Inf}` which are used here to provide some short proofs.