mathlib

ee72cf62 - refactor(order/compactly_generated): Generalize `submodule.exists_finset_of_mem_supr` to compact elements of complete lattices (#15419)

refactor(order/compactly_generated): Generalize `submodule.exists_finset_of_mem_supr` to compact elements of complete lattices (#15419) The lemma `submodule.exists_finset_of_mem_supr` can be generalized to compact elements of complete lattices. This should make it easy to get analogous results for other algebraic structures.