isArtinian_iSup — Mathlib

English

If M_i is Artinian for each i in a finite index set, then the supremum of submodules ⨆ i, M_i is Artinian.

Русский

Если каждый M_i артинанов по i в конечном индексе, то ⨆ i, M_i артинанов.

LaTeX

$$$(\\forall i, IsArtinian\\ R (M i)) \\Rightarrow IsArtinian\\ R (\\bigsqcup_i M_i)$$$

Lean4

instance isArtinian_iSup : ∀ {M : ι → Submodule R P} [∀ i, IsArtinian R (M i)], IsArtinian R ↥(⨆ i, M i) :=
  by
  apply Finite.induction_empty_option _ _ _ ι
  · intro _ _ e h _ _; rw [← e.iSup_comp]; apply h
  · intros; rw [iSup_of_empty]; infer_instance
  · intro _ _ ih _ _; rw [iSup_option]; infer_instance

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