English
The submodule generated by a supremum over a finite index set of finite-dimensional submodules is finite-dimensional.
Русский
Подпространство, порожденное верхней границей по сквозной системе, конечномерно.
LaTeX
$$$ finiteDimensional_iSup {ι} [Finite ι] (S : ι → Submodule K V) [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (↑(⨆ i, 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 finiteDimensional_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule K V)
[∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (s.sup S : Submodule K V) :=
by
refine
@Finset.sup_induction _ _ _ _ s S (fun i => FiniteDimensional K ↑i) (finiteDimensional_bot K V) ?_ fun i _ => by
infer_instance
intro S₁ hS₁ S₂ hS₂
exact Submodule.finiteDimensional_sup S₁ S₂
