Commit 2023-07-01 12:38 a7c79b4c

feat: Add finite iff bounded lemmas (#5567) This PR adds a lemma stating that finiteness is equivalent to boundedness above and below in a locally finite lattice, as well as one-way versions for both types of semilattice.