feat(order/compactly_generated): Show that the sublattice below a compact element is coatomic (#5942)
feat(order/compactly_generated): Show that the sublattice below a compact element is coatomic (#5942)

Show that the sublattice below a compact element is coatomic. Introduce a lemma stating that any set lying strictly below a compact element has Sup strictly below that element.

<!--
put comments you want to keep out of the PR commit here.
If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->




leanprover-community/mathlib,leanprover-community/mathlib