finiteDimensional_iSup_of_finite — Mathlib

English

If ι is finite and each t_i is finite-dimensional over K, then the supremum ⨆ i t_i is finite-dimensional over K: FiniteDimensional K (⨆ i, t_i).

Русский

Если индексный набор конечен и каждый t_i имеет конечную размерность над K, то ⨆ i t_i имеет конечную размерность над K: FiniteDimensional K (⨆ i, t_i).

LaTeX

$$$\operatorname{FiniteDimensional}_K(\bigsup_i t_i)$$$

Lean4

instance finiteDimensional_iSup_of_finite [h : Finite ι] [∀ i, FiniteDimensional K (t i)] :
    FiniteDimensional K (⨆ i, t i : IntermediateField K L) :=
  by
  rw [← iSup_univ]
  induction Set.univ, Set.finite_univ (α := ι) using Set.Finite.induction_on with
  | empty =>
    rw [iSup_emptyset]
    exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional
  | insert s hs =>
    rw [iSup_insert]
    exact IntermediateField.finiteDimensional_sup _ _

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