instContainsZeroIsArtinianObjectOfHasZeroObject

English

If the ambient category has a zero object, then the class of Artinian objects contains a zero subobject.

Русский

Если в окружении есть нулевой объект, то класс артинянных объектов содержит нулевой подобъект.

LaTeX

$$$[HasZeroObject\\; C] \\Rightarrow (\\mathrm{isArtinianObject}.ContainsZero)$$$

Lean4

instance [HasZeroObject C] : (isArtinianObject (C := C)).ContainsZero where
  exists_zero :=
    ⟨0, isZero_zero _, by
      rw [← isArtinianObject.is_iff]
      exact isArtinianObject_of_isZero (isZero_zero C)⟩

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