Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-17 00:03 f1b687cd

View on Github →

feat (order/order_iso): lemmas about order_isos on lattices (#3397) shows that order_embeddings and order_isos respect lattice operations

Estimated changes

Modified src/order/order_iso.lean

added theorem order_embedding.le_map_sup

added theorem order_embedding.map_inf_le

added theorem order_iso.map_bot

added theorem order_iso.map_inf

added theorem order_iso.map_sup

added theorem order_iso.map_top