Mathlib v3 is deprecated. Go to Mathlib v4

Theorem galois_connection.decreasing_l_u

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
Deleted galois_connection.decreasing_l_uView on Github →
2018-01-11 16:26
order/galois_connection.lean
refactor(order/basic): remove "increasing/decreasing" unusual defs
Modified galois_connection.decreasing_l_uView on Github →
2017-08-11 18:26
order/galois_connection.lean
add Galois connection, also add a couple of order theoretic results
Added galois_connection.decreasing_l_uView on Github →