isNoetherianObject_iff_not_strictMono

English

IsNoetherianObject X is equivalent to the statement that every sequence f: Nat → Subobject(X) is not strictly monotone.

Русский

Объект X нётерановский тогда и только тогда, когда любая последовательность f: Nat → Subobject(X) не строго монотонна.

LaTeX

$$$\text{IsNoetherianObject}(X) \iff \forall f: \mathbb{N} \to \mathrm{Subobject}(X),\ \neg \mathrm{StrictMono}(f).$$$

Lean4

theorem isNoetherianObject_iff_not_strictMono : IsNoetherianObject X ↔ ∀ (f : ℕ → Subobject X), ¬StrictMono f :=
  by
  refine ⟨fun _ ↦ not_strictMono_of_wellFoundedGT, fun h ↦ ?_⟩
  dsimp only [IsNoetherianObject]
  rw [ObjectProperty.is_iff, isNoetherianObject, WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
  exact ⟨fun f ↦ h f.toFun (fun a b h ↦ f.map_rel_iff.2 h)⟩

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