finite

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#AffineBasis.finite

English

If the vector space V is finite-dimensional, then the index set ι of an affine basis is finite.

Русский

Если V конечноразмерно, то множество индексов ι аффинной базы также конечное.

LaTeX

$$Finite ι$$

Lean4

protected theorem finite [FiniteDimensional k V] (b : AffineBasis ι k P) : Finite ι :=
  finite_of_fin_dim_affineIndependent k b.ind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru