Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-10 15:58 4a59a4d4

View on Github →

chore(order/galois_connection): Make lifting instances reducible (#12559) and provide infi₂ and supr₂ versions of the lemmas.

Estimated changes

modified theorem galois_connection.l_Sup
modified theorem galois_connection.l_supr
modified theorem galois_connection.u_Inf
modified theorem galois_connection.u_infi