isNoetherian_iSup — Mathlib

English

If each M_i is Noetherian, then the supremum (iSup) of the family {M_i} is Noetherian.

Русский

Если каждый M_i — Noetherian, то их объединение по iSup — Noetherian.

LaTeX

$$$[\forall i, IsNoetherian R (M_i)] \Rightarrow IsNoetherian R (\bigsqcup_i M_i)$$$

Lean4

instance isNoetherian_iSup : ∀ {M : ι → Submodule R P} [∀ i, IsNoetherian R (M i)], IsNoetherian 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

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