Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-28 16:27 1417a74e

View on Github →

feat(order/galois_connection): add 2 lemmas (#17221) add galois_connection.u_eq_top and galois_connection.l_eq_bot

Estimated changes

Modified src/order/galois_connection.lean

modified theorem galois_connection.l_bot

added theorem galois_connection.l_eq_bot

added theorem galois_connection.u_eq_top

modified theorem galois_connection.u_top