Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-04 08:58 5d0e65aa

View on Github →

chore(order/galois_connection): upgrade is_glb_l to is_least_l (#10606)

  • upgrade galois_connection.is_glb_l to galois_connection.is_least_l;
  • upgrade galois_connection.is_lub_l to galois_connection.is_greatest_l.

Estimated changes

modified theorem galois_connection.is_glb_l
modified theorem galois_connection.is_lub_u