instIsClosedUnderSubobjectsIsArtinianObject

English

The property of being Artinian is closed under taking subobjects: subobjects of an Artinian object are Artinian.

Русский

Свойство артинянности замкнуто относительно подобъектов: подобъект артинянного объекта также артинян.

LaTeX

$$$\\forall X [\\mathrm{IsArtinianObject}(X)],\\forall S \\le X:\\ \\mathrm{IsArtinianObject}(S)$$$

Lean4

instance : (isArtinianObject (C := C)).IsClosedUnderSubobjects where
  prop_of_mono f _
    hY := by
    rw [← isArtinianObject.is_iff] at hY ⊢
    exact isArtinianObject_of_mono f

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