mathlib3

e726945e - refactor(order/atoms): is_simple_order from is_simple_lattice (#10537)

refactor(order/atoms): is_simple_order from is_simple_lattice (#10537) Rename `is_simple_lattice` to `is_simple_order`, still stating that every element is either `bot` or `top` are, and that it is nontrivial. To state `is_simple_order`, `has_le` and `bounded_order` are required to be defined. This allows for an order where `⊤ ≤ ⊥` (the always true order). Many proofs/statements about `is_simple_order`s have been generalized to require solely `partial_order` and not `lattice`. The statements themselves have not been changed. The `is_simple_order.distrib_lattice` instance has been downgraded into a `def` to prevent loops. Helper defs have been added like `is_simple_order.preorder` (which is true given the `has_le` `bounded_order` axioms) `is_simple_order.linear_order`, and `is_simple_order.lattice` (which are true when `partial_order`, implying `⊥ < ⊤`.). Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>