isArtinianObject_iff_not_strictAnti

English

X is Artinian iff there is no infinite strictly antitone chain of subobjects of X.

Русский

X артинян, если и только если не существует бесконечной строгой антицепи подобъектов X.

LaTeX

$$$\\mathrm{IsArtinianObject}(X) \\iff \\forall f: \\mathbb{N} \\to \\mathrm{Subobject}(X), \\neg \\mathrm{StrictAnti}(f)$$$

Lean4

theorem isArtinianObject_iff_not_strictAnti : IsArtinianObject X ↔ ∀ (f : ℕ → Subobject X), ¬StrictAnti f :=
  by
  refine ⟨fun _ ↦ not_strictAnti_of_wellFoundedLT, fun h ↦ ?_⟩
  dsimp only [IsArtinianObject]
  rw [ObjectProperty.is_iff, isArtinianObject, WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
  exact ⟨fun f ↦ h f.toFun (fun a b h ↦ f.map_rel_iff.2 h)⟩

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