isNoetherian_of_le — Mathlib

English

If s ≤ t and t is Noetherian, then s is Noetherian; and conversely for supersets given FG conditions.

Русский

Если s ⊆ t и t Ноетерен, то s также Ноетерен; аналогично в противном направлении при FG.

LaTeX

$$$\text{Noetherian}(s) \Leftarrow \text{Noetherian}(t)$ under inclusion with FG$$

Lean4

theorem isNoetherian_of_le {s t : Submodule R M} [ht : IsNoetherian R t] (h : s ≤ t) : IsNoetherian R s :=
  isNoetherian_submodule.mpr fun _ hs' => isNoetherian_submodule.mp ht _ (le_trans hs' h)

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