mathlib3

9117ad71 - feat(order/atoms): define (co)atomic, (co)atomistic lattices (#5588)

feat(order/atoms): define (co)atomic, (co)atomistic lattices (#5588) Define (co)atomic, (co)atomistic lattices Relate these lattice definitions Provide basic subtype instances Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>