fg_finset_sup — Mathlib

English

If s is a finite set and N i are submodules with each (N i).FG, then the Finset supremum (s.sup N) is FG.

Русский

Для конечного множества s и подмодулей N i, если каждый (N i).FG, то (s.sup N).FG.

LaTeX

$$∀ {ι} (s : Finset ι) (N : ι → Submodule R M), (∀ i ∈ s, (N i).FG) → (s.sup N).FG$$

Lean4

theorem fg_finset_sup {ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) : (s.sup N).FG :=
  Finset.sup_induction fg_bot (fun _ ha _ hb => ha.sup hb) h

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