isArtinian_sup — Mathlib

English

If M1 and M2 are Artinian submodules of P, then their supremum M1 ⊔ M2 is Artinian.

Русский

Если M1 и M2 — артинановы подмодули P, то их наибольшая сумма M1 ⊔ M2 артинаново.

LaTeX

$$$IsArtinian\\ R\\ M_1 \\land IsArtinian\\ R\\ M_2 \\Rightarrow IsArtinian\\ R\\ (M_1 \\ ⊔ \\ M_2)$$$

Lean4

instance isArtinian_sup (M₁ M₂ : Submodule R P) [IsArtinian R M₁] [IsArtinian R M₂] : IsArtinian R ↥(M₁ ⊔ M₂) :=
  by
  have := isArtinian_range (M₁.subtype.coprod M₂.subtype)
  rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this

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