finiteDimensional_pi — Mathlib

English

If V is finite-dimensional, then the function space V^ι is finite-dimensional for any finite index set ι.

Русский

Если пространство V конечномерно, то пространство функций V^ι конечномерно для любого конечного множителя ι.

LaTeX

$$FiniteDimensional(K, V) ⇒ FiniteDimensional(K, ι → V)$$

Lean4

instance finiteDimensional_pi {ι : Type*} [Finite ι] : FiniteDimensional K (ι → K) :=
  Finite.pi

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