Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 04:12 2c5d4a3c

View on Github →

chore(order/rel_iso): add a few lemmas (#5106)

add lemmas order_iso.apply_eq_iff_eq etc;
define order_iso.symm.

Estimated changes

Modified src/data/finsupp/lattice.lean

Modified src/order/galois_connection.lean

Modified src/order/rel_iso.lean

added theorem order_embedding.le_map_sup

added theorem order_embedding.map_inf_le

added theorem order_iso.apply_eq_iff_eq

added theorem order_iso.apply_le_apply

added theorem order_iso.apply_lt_apply

added theorem order_iso.apply_symm_apply

added theorem order_iso.map_inf

added theorem order_iso.map_sup

added theorem order_iso.map_top

added def order_iso.symm

added theorem order_iso.symm_apply_apply

deleted theorem rel_embedding.le_map_sup

deleted theorem rel_embedding.map_inf_le

deleted theorem rel_iso.map_inf

deleted theorem rel_iso.map_sup

deleted theorem rel_iso.map_top