Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order_iso.to_galois_connection

Modification history

2020-08-21 16:04
src/order/galois_connection.lean
feat(order/rel_iso): a new definition of order_iso, using preorder instances (#3838) …
Added order_iso.to_galois_connectionView on Github →
2020-08-16 03:16
src/order/galois_connection.lean
chore(order/rel_iso): rename order_iso and order_embedding to rel_iso and rel_embedding (#3750) …
Deleted order_iso.to_galois_connectionView on Github →
2020-03-02 10:42
src/order/galois_connection.lean
feat(order/galois_connection): lemmas about galois insertions and supr/infi (#2052) …
Modified order_iso.to_galois_connectionView on Github →
2019-09-26 12:04
src/order/galois_connection.lean
feat(data/setoid): create file about setoids (#1453) …
Added order_iso.to_galois_connectionView on Github →