mathlib

79ca6e23 - 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] -->