finite_set

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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

← MathLib Explorer

English

For an affine basis b with index set s ⊆ ι, the set s is finite whenever V is finite-dimensional.

Русский

Для аффинной базы b с индексным множеством s ⊆ ι множество s конечно.

LaTeX

$$s.Finite$$

Lean4

protected theorem finite_set [FiniteDimensional k V] {s : Set ι} (b : AffineBasis s k P) : s.Finite :=
  finite_set_of_fin_dim_affineIndependent k b.ind

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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