Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 02:30 731c26f2

View on Github →

refactor(*): swap sides of iff in {rel_embedding,order_embedding}.map_rel_iff (#5556) This way RHS is "simpler" than LHS. Other API changes (in rel_embedding and/or ord_embedding and/or rel_iso and/or ord_iso namespaces):

  • drop map_le_iff, rename apply_le_apply to le_iff_le;
  • drop map_lt_iff, rename apply_lt_apply to lt_iff_lt;
  • rename apply_eq_apply to eq_iff_eq.

Estimated changes

deleted theorem order_iso.apply_le_apply
deleted theorem order_iso.apply_lt_apply
added theorem order_iso.le_iff_le
added theorem order_iso.lt_iff_lt
modified theorem rel_embedding.map_rel_iff
modified theorem rel_iso.coe_fn_mk
added theorem rel_iso.eq_iff_eq
deleted theorem rel_iso.map_rel_iff''
modified theorem rel_iso.map_rel_iff