isNoetherianObject_iff_monotone_chain_condition

English

IsNoetherianObject X is equivalent to the statement that every monotone chain of subobjects of X stabilizes: for every f : Nat → Subobject(X), there exists n such that for all m ≥ n, f(m) = f(n).

Русский

Объект X нётерановский тогда и только тогда, когда любая монотонная цепь подобъектов X стабилизируется: для всякой f : Nat → Subobject(X) существует n, такое что для всех m ≥ n выполняется f(m) = f(n).

LaTeX

$$$\text{IsNoetherianObject}(X) \iff \forall f: \mathbb{N} \to_o \mathrm{Subobject}(X),\ \exists n:\mathbb{N},\ \forall m:\mathbb{N},\ n \le m \Rightarrow f(n)=f(m).$$$

Lean4

theorem isNoetherianObject_iff_monotone_chain_condition :
    IsNoetherianObject X ↔ ∀ (f : ℕ →o Subobject X), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m :=
  by
  dsimp only [IsNoetherianObject]
  rw [ObjectProperty.is_iff, isNoetherianObject, wellFoundedGT_iff_monotone_chain_condition]

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