refactor(order/conditionally_complete_lattice): refactor definition, add constructors

[urkud]

Conditionally complete lattices

• reformulate the definition of conditionally_complete_lattice in terms of is_lub/is_glb; this way all instances in mathlib become shorter;
• add a new constructor conditionally_complete_lattice_of_is_lub_of_rel_iso and use it for reals and integers;
• add lemmas is_lub_csupr, is_lub_csupr_set, is_lub.csupr_eq, is_lub.csupr_set_eq, and their analogues for infi;
• add is_greatest.Sup_mem and is_least.Inf_mem;
• golf some proofs about nat, use named properties like bdd_above and set.nonempty;
• add nat.is_least_Inf, nat.is_lub_Sup, and nat.is_greatest_Sup.

Real numbers

• drop lemmas like real.Sup_le when they are not better than lemmas from order.conditionally_complete_order;
• drop bdd_above/bdd_below assumptions in real.add_neg_lt_Sup and real.lt_Inf_add_pos;

Other changes

• add set.inv_empty, set.inv_univ, set.neg_empty, set.neg_univ;
• add function.surjective.nonempty_preimage and function.monotone_eval;
• add is_lub_pi and is_glb_pi

---

• depends on: [Merged by Bors] - feat(algebra/ordered_group): add order_iso.inv #8492
• depends on: [Merged by Bors] - chore(data/int): move some lemmas from basic to a new file #8495
• depends on: [Merged by Bors] - chore(data/real/basic): cleanup #8501
• add nat.is_greatest_Sup

[github-actions]

This PR/issue depends on:

• [Merged by Bors] - feat(algebra/ordered_group): add order_iso.inv #8492
• [Merged by Bors] - chore(data/int): move some lemmas from basic to a new file #8495
• [Merged by Bors] - chore(data/real/basic): cleanup #8501
  By Dependent Issues (🤖). Happy coding!