isArtinian_of_le — Mathlib

English

If s ≤ t are submodules of M and t is Artinian, then s is Artinian.

Русский

Если s ≤ t — подмодуля M и t артинарен, то s также артинан.

LaTeX

$$$\\forall s,t \\le M: s \\le t \\to \\mathrm{IsArtinian}_R(t) \\to \\mathrm{IsArtinian}_R(s)$$$

Lean4

theorem isArtinian_of_le {s t : Submodule R M} [IsArtinian R t] (h : s ≤ t) : IsArtinian R s :=
  isArtinian_of_injective (Submodule.inclusion h) (Submodule.inclusion_injective h)

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