Mathlib v3 is deprecated. Go to Mathlib v4

Structure galois_insertion

Modification history

2018-08-18 12:55

order/galois_connection.lean

feat(order/galois_connection): add Galois insertion and lattice lifts along a Galois insertion

Added galois_insertion View on Github →