mathlib3

0104948e - feat(order/atoms): further facts about atoms, coatoms, and simple lattices (#5493)

feat(order/atoms): further facts about atoms, coatoms, and simple lattices (#5493) Provides possible instances of `bounded_distrib_lattice`, `boolean_algebra`, `complete_lattice`, and `complete_boolean_algebra` on a simple lattice Relates the `is_atom` and `is_coatom` conditions to `is_simple_lattice` structures on intervals Shows that all three conditions are preserved by `order_iso`s Adds more instances on `bool`, including `is_simple_lattice` Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>