Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 13:05 7a031718

View on Github →

chore(order/rel_iso): add some missing lemmas (#5492) Also define order_iso.trans.

Estimated changes

Modified src/order/rel_iso.lean

added theorem order_embedding.coe_subtype

added def order_embedding.subtype

added theorem order_iso.coe_trans

added theorem order_iso.map_bot'

modified theorem order_iso.map_bot

added theorem order_iso.map_top'

modified theorem order_iso.map_top

added theorem order_iso.symm_apply_eq

added theorem order_iso.symm_injective

added theorem order_iso.symm_symm

added def order_iso.trans

added theorem order_iso.trans_apply

added theorem rel_embedding.coe_trans

modified theorem rel_embedding.trans_apply

added theorem rel_iso.default_def

deleted def set_coe_embedding