English
The supremum (sum) of a finite family of finite submodules is finite.
Русский
Супремум (сума) конечной семьи конечных подподмодулей конечен.
LaTeX
$$$\\forall s\\in\\mathrm{Finset}\\; I\\; (S_i)\\; [\\forall i, Module.Finite R (S_i)]\\; \\Rightarrow\\; Module.Finite R (\\sum_{i \\in s} S_i)$$
Lean4
/-- The submodule generated by a finite supremum of finite-dimensional submodules is
finite-dimensional.
Note that strictly this only needs `∀ i ∈ s, FiniteDimensional K (S i)`, but that doesn't
work well with typeclass search. -/
instance finite_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule R V) [∀ i, Module.Finite R (S i)] :
Module.Finite R (s.sup S : Submodule R V) :=
by
refine
@Finset.sup_induction _ _ _ _ s S (fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_ fun i _ => by
infer_instance
intro S₁ hS₁ S₂ hS₂
exact Submodule.finite_sup S₁ S₂
