Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 03:16 ae8abf37

View on Github →

chore(order/rel_iso): rename order_iso and order_embedding to rel_iso and rel_embedding (#3750) renames order_iso and order_embedding, to make it clear they apply to all binary relations makes room for a new definition of order_embedding that will deal with order instances

Estimated changes

deleted theorem injective_of_increasing
deleted theorem order_embedding.coe_fn_mk
deleted theorem order_embedding.injective
deleted theorem order_embedding.ord
deleted structure order_embedding
deleted theorem order_iso.apply_inv_self
deleted theorem order_iso.coe_coe_fn
deleted theorem order_iso.coe_fn_mk
deleted theorem order_iso.coe_fn_symm_mk
deleted theorem order_iso.coe_fn_to_equiv
deleted theorem order_iso.coe_mul
deleted theorem order_iso.coe_one
deleted theorem order_iso.ext
deleted theorem order_iso.inv_apply_self
deleted theorem order_iso.map_bot
deleted theorem order_iso.map_inf
deleted theorem order_iso.map_sup
deleted theorem order_iso.map_top
deleted theorem order_iso.mul_apply
deleted theorem order_iso.ord''
deleted theorem order_iso.ord
deleted theorem order_iso.refl_apply
deleted theorem order_iso.rel_symm_apply
deleted def order_iso.rsymm
deleted theorem order_iso.symm_apply_rel
deleted theorem order_iso.trans_apply
deleted structure order_iso
deleted theorem preimage_equivalence
deleted def set_coe_embedding
deleted def subrel
deleted theorem subrel_val
added theorem preimage_equivalence
added structure rel_embedding
added theorem rel_iso.apply_inv_self
added theorem rel_iso.coe_coe_fn
added theorem rel_iso.coe_fn_mk
added theorem rel_iso.coe_fn_symm_mk
added theorem rel_iso.coe_mul
added theorem rel_iso.coe_one
added theorem rel_iso.ext
added theorem rel_iso.inv_apply_self
added theorem rel_iso.map_bot
added theorem rel_iso.map_inf
added theorem rel_iso.map_rel_iff''
added theorem rel_iso.map_rel_iff
added theorem rel_iso.map_sup
added theorem rel_iso.map_top
added theorem rel_iso.mul_apply
added theorem rel_iso.refl_apply
added theorem rel_iso.rel_symm_apply
added def rel_iso.rsymm
added theorem rel_iso.symm_apply_rel
added theorem rel_iso.trans_apply
added structure rel_iso
added def subrel
added theorem subrel_val
deleted theorem order_iso.cof.aux
deleted theorem order_iso.cof
modified theorem ordinal.cof_cof
added theorem rel_iso.cof.aux
added theorem rel_iso.cof