Artinian/noetherian lattice

Stream: Is there code for X?

[Jesse Vogel]

Does there exist a notion of artinian/noetherian lattice/preorder? That is, a lattice for which every descending/ascending chain has finite length (maybe refering to acc ?). Maybe then is_noetherian and is_artinian could be defined in terms of these notions?

[Andrew Yang]

docs#well_founded

[Andrew Yang]

Also docs#is_noetherian_iff_well_founded and docs#is_artinian_iff_well_founded.

[Andrew Yang]

docs#well_founded.well_founded_iff_has_max' and its friends should be useful as well if you want to show that all noetherian-and-artinian modules have finite composition series.