isArtinianObject_iff_antitone_chain_condition

English

For an object X in a category, IsArtinianObject X is equivalent to the antitone chain condition: every order-preserving map f: ℕ →o Subobject(X)ᵒᵈ stabilizes eventually, i.e., there exists n such that f(n)=f(m) for all m≥n.

Русский

Для объекта X в категории IsArtinianObject X эквивалентно антинотельному условию цепи: любая монотонно возрастaющая функция f: ℕ →o Subobject(X)ᵒᵈ стабилизируется, то есть существует n, для которого f(n)=f(m) при m≥n.

LaTeX

$$$\text{IsArtinianObject } X \iff \forall f: \mathbb{N} \to_o (\mathrm{Subobject}(X))^{\mathrm{op}}, \exists n\, \forall m\ge n, f(n)=f(m)$$$

Lean4

theorem isArtinianObject_iff_antitone_chain_condition :
    IsArtinianObject X ↔ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m :=
  by
  dsimp only [IsArtinianObject]
  rw [ObjectProperty.is_iff, isArtinianObject, ← wellFoundedGT_dual_iff, wellFoundedGT_iff_monotone_chain_condition]

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