Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-02 10:42 2683fa09

View on Github →

feat(order/galois_connection): lemmas about galois insertions and supr/infi (#2052)

  • feat(order/galois_connection): lemmas about galois insertions and supr/infi
  • Fix build, hopefully

Estimated changes

modified theorem galois_insertion.l_u_eq