mathlib

d82b8787 - chore(category_theory/category/preorder): split material on galois connections (#17339)

chore(category_theory/category/preorder): split material on galois connections (#17339) This is reducing unnecessary imports. Really, however, someone should tackle `order.complete_lattice`, which has unnecessary heavy imports. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>