instWellFoundedGTSubobjectOfIsNoetherianObject

English

If X is a Noetherian object, then Subobject(X) is well-founded with respect to the reverse inclusion order; i.e., there is no infinite strictly descending chain of subobjects.

Русский

Если X — нётеровский объект, то Subobject(X) по отношению включения является хорошо упорядоченным с точки зрения ниспадающих цепей; т.е. бесконечной строго убывающей цепи подобъектов не существует.

LaTeX

$$$\text{IsNoetherianObject}(X) \Rightarrow \mathrm{WellFoundedGT}(\mathrm{Subobject}(X)).$$$

Lean4

instance [IsNoetherianObject X] : WellFoundedGT (Subobject X) :=
  isNoetherianObject.prop_of_is X

Похожие утверждения