Commit 2024-10-09 07:18 77a0e208

feat: in a WellFoundedLT CompleteLattice, Independent sets are finite (#17525) The same conclusion was previously known under a WellFounded (· > ·) assumption, which we replace with WellFoundedGT. We also change WellFounded in existing lemma names to WellFoundedGT to avoid confusion with the new WellFoundedLT lemmas we introduce. A consequence is that a direct sum of infinitely many nontrivial modules can't be Artinian. (Previous results imply it can't be Noetherian.) The lemma Disjoint.right_lt_sup_of_left_ne_bot is used and added. The definition of NoetherianSpace is changed to use WellFoundedGT (defeq to before), and the statement of noetherianSpace_TFAE is changed to use WellFoundedLT.