isArtinianObject_of_isZero

Mathlib.CategoryTheory.Subobject.ArtinianObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isArtinianObject_of_isZero

← MathLib Explorer

English

A zero object is Artinian.

Русский

Нулевой объект является артинянным.

LaTeX

$$$\\text{IsZero}(X) \\Rightarrow \\mathrm{IsArtinianObject}(X)$$$

Lean4

theorem isArtinianObject_of_isZero (hX : IsZero X) : IsArtinianObject X :=
  by
  rw [isArtinianObject_iff_antitone_chain_condition]
  have := Subobject.subsingleton_of_isZero hX
  intro f
  exact ⟨0, fun m hm ↦ Subsingleton.elim _ _⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru