Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 08:17 3f5a348f

View on Github →

chore(galois_connection): golf some proofs (#8582)

  • golf some proofs
  • add galois_insertion.left_inverse_l_u and galois_coinsertion.left_inverse_u_l;
  • drop galois_insertion.l_supr_of_ul_eq_self and galois_coinsertion.u_infi_of_lu_eq_self: these lemmas are less general than galois_connection.l_supr and galois_connection.u_infi.

Estimated changes

modified theorem galois_connection.l_bot
modified theorem galois_connection.u_Inf
modified theorem galois_connection.u_inf
modified theorem galois_connection.u_infi
modified theorem galois_connection.u_top