mem_spanPoints

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

← MathLib Explorer

English

If a point p belongs to a set s, then p belongs to spanPoints k s.

Русский

Если точка p принадлежит множеству s, то она принадлежит spanPoints k s.

LaTeX

$$$p\\in s \\;\\Rightarrow\\; p \\in spanPoints(k,s)$$$

Lean4

/-- A point in a set is in its affine span. -/
theorem mem_spanPoints (p : P) (s : Set P) : p ∈ s → p ∈ spanPoints k s
  | hp => ⟨p, hp, 0, Submodule.zero_mem _, (zero_vadd V p).symm⟩

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

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

Разделы

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

Аффилиация

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