finiteDimensional_iSup_of_finset — Mathlib

English

If s is a finite set of indices and each t_i is finite-dimensional over K, then ⨆ i∈s t_i is finite-dimensional over K: FiniteDimensional K (⨆ i∈s, t_i).

Русский

Если i варьируется по конечному множеству s и каждый t_i имеет конечную размерность над K, то ⨆ i∈s t_i имеет конечную размерность над K.

LaTeX

$$$\operatorname{FiniteDimensional}_K\big(\bigsup_{i\in s} t_i\big)$$$

Lean4

/-- See `finiteDimensional_iSup_of_finset'` for a stronger version,
that was the one used in mathlib3. -/
instance finiteDimensional_iSup_of_finset {s : Finset ι} [∀ i, FiniteDimensional K (t i)] :
    FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L) :=
  iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite

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