Mathlib v3 is deprecated. Go to Mathlib v4

Theorem galois_connection.increasing_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
Deleted galois_connection.increasing_u_lView on Github →
2018-01-11 16:26
order/galois_connection.lean
refactor(order/basic): remove "increasing/decreasing" unusual defs
Modified galois_connection.increasing_u_lView 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.increasing_u_lView on Github →