induction — Mathlib

English

If for every submodule I, the property P(I) follows from P(J) for all J < I, then P(I) holds for all submodules.

Русский

Если для каждого подмодуля I свойство P(I) следует из свойств P(J) для всех J < I, то P(I) выполняется для всех подмодулей.

LaTeX

$$$\\forall P, (\\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 {P : Submodule R M → Prop} (hgt : ∀ I, (∀ J < I, P J) → P I) (I : Submodule R M) : P I :=
  WellFoundedLT.induction I hgt

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