Mathlib v3 is deprecated. Go to Mathlib v4

Theorem galois_connection.le_u_l

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_connection.le_u_l View on Github →