Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-09 20:30 d04429fa

View on Github →

chore(logic/embedding,order/order_iso): review (#2618)

  • swap inj with inj' to match other bundled homomorphisms;
  • make some arguments explicit to avoid embedding.of_surjective _ in the pretty printer output;
  • make set_value computable.

Estimated changes

deleted theorem function.embedding.inj'
added theorem function.embedding.inj
added theorem order_embedding.inj
deleted theorem order_embedding.ord'
added theorem order_embedding.ord
deleted theorem order_iso.ord'
added theorem order_iso.ord