not_strictMono_of_isNoetherianObject

English

If X is Noetherian, then for any f: Nat → Subobject(X), not StrictMono f holds.

Русский

Если X нётеровский, то для любого f: Nat → Subobject(X) выполняется не StrictMono f.

LaTeX

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

Lean4

theorem not_strictMono_of_isNoetherianObject [IsNoetherianObject X] (f : ℕ → Subobject X) : ¬StrictMono f :=
  (isNoetherianObject_iff_not_strictMono X).1 inferInstance f

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