subset_affineSpan

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#subset_affineSpan

English

A set is contained in its affine span.

Русский

Множество содержится в своем афинном span.

LaTeX

$$$s \\subseteq \\operatorname{affineSpan}_k s$$$

Lean4

/-- A set is contained in its affine span. -/
theorem subset_affineSpan (s : Set P) : s ⊆ affineSpan k s :=
  subset_spanPoints k s

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

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

Разделы

Аффилиация

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