[Merged by Bors] - feat: in a WellFoundedLT CompleteLattice, Independent sets are finite#17525
[Merged by Bors] - feat: in a WellFoundedLT CompleteLattice, Independent sets are finite#17525alreadydone wants to merge 5 commits intomasterfrom
Conversation
PR summary afb937f300Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
…#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`.
|
Pull request successfully merged into master. Build succeeded: |
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_botis used and added.The definition of
NoetherianSpaceis changed to useWellFoundedGT(defeq to before), and the statement ofnoetherianSpace_TFAEis changed to useWellFoundedLT.