Mathlib v3 is deprecated. Go to Mathlib v4

Def bounded_order.lift

Modification history

2022-02-22 10:50
src/order/bounded_order.lean
feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149) …
Modified bounded_order.liftView on Github →
2022-02-21 13:33
src/order/complete_lattice.lean
feat(order/*): Missing order lifting instances (#12154) …
Added bounded_order.liftView on Github →