introduce the category of Bounded posets

[fchapoton]

as an useful thing to have

also declare that finite lattices are bounded

:memo: Checklist

• [x] The title is concise and informative.
• [x] The description explains in detail what this PR is about.
• [x] I have created tests covering the changes.
• [x] I have updated the documentation and checked the documentation preview.

[fchapoton]

Would it be better to put "Bounded" lower in the list of axiom names ?

EDIT: It seems not.

[fchapoton]

Here is a way to make the "bounded finite" disappear.

EDIT: namely I moved "Bounded" before "Finite" in the list of axioms.