English
If each S i is finite-dimensional, then the sup over a finite set s is finite-dimensional; supports finset induction over i.
Русский
Если каждый S_i конечномерен, то сумма по конечному множеству s тоже конечномерна; поддерживает индукцию по Finset.
LaTeX
$$$ finiteDimensional_finset_sup {ι} (s : Finset ι) (S : ι → Submodule K V) [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (s.sup S : Submodule K V) $$$
Lean4
/-- The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite
sort is finite-dimensional. -/
instance finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → Submodule K V) [∀ i, FiniteDimensional K (S i)] :
FiniteDimensional K ↑(⨆ i, S i) := by
cases nonempty_fintype (PLift ι)
rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]
exact Submodule.finiteDimensional_finset_sup _ _
