Mathlib v3 is deprecated. Go to Mathlib v4

Def order_iso.with_top_congr

Modification history

2022-03-05 13:15
src/order/hom/basic.lean
feat(order/hom/basic): add `order_iso.with_{top,bot}_congr` (#12264) …
Added order_iso.with_top_congrView on Github →