Mathlib v3 is deprecated. Go to Mathlib v4

Theorem galois_connection.l_u_le

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