English
If P is a property of submodules of M such that for every I, if P holds for all J > I then P holds for I, then P holds for all submodules of M. This is the induction principle on Noetherian modules.
Русский
Если свойство P подмодулей M удовлетворяет условию: для каждого I, если P выполняется для всех J > I, то P выполняется и для I, то P выполняется для всех подмодулей M.
LaTeX
$$$[IsNoetherian R M]\Rightarrow (\forall P: Submodule R M \to \text{Prop}, (\forall I, (\forall J > I, P(J)) \Rightarrow P(I)) \Rightarrow \forall I, P(I))$$$
Lean4
/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
theorem induction [IsNoetherian R M] {P : Submodule R M → Prop} (hgt : ∀ I, (∀ J > I, P J) → P I) (I : Submodule R M) :
P I :=
IsWellFounded.induction _ I hgt
