feat(topology/order): if `e` is an equiv, `induced e.symm = coinduced e` (#13272)
feat(topology/order): if `e` is an equiv, `induced e.symm = coinduced e` (#13272)






leanprover-community/mathlib,leanprover-community/mathlib