finiteDimensional_direction_affineSpan

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#Coplanar.finiteDimensional_direction_affineSpan

← MathLib Explorer

English

Collinear points are coplanar.

Русский

Коллинеарные точки лежат на одной плоскости.

LaTeX

$$Collinear(k,s) → Coplanar(k,s)$$

Lean4

/-- The direction of the affine span of coplanar points is finite-dimensional. -/
theorem finiteDimensional_direction_affineSpan {s : Set P} (h : Coplanar k s) :
    FiniteDimensional k (affineSpan k s).direction :=
  (direction_affineSpan k s).symm ▸ h.finiteDimensional_vectorSpan

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

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

Разделы

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

Аффилиация

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