mem_affineSpan

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

← MathLib Explorer

English

A point in a set is in its affine span.

Русский

Точка из множества принадлежит его афинному span.

LaTeX

$$$p \\in s \\Rightarrow p \\in \\operatorname{affineSpan}_k s$$$

Lean4

/-- A point in a set is in its affine span. -/
theorem mem_affineSpan {p : P} {s : Set P} (hp : p ∈ s) : p ∈ affineSpan k s :=
  mem_spanPoints k p s hp

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

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

Разделы

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

Аффилиация

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