span_univ

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#AffineSubspace.span_univ

English

The affine span of the entire space is the top subspace.

Русский

Аффинная оболочка все пространства есть верхнее подпространство.

LaTeX

$$$\\mathrm{affineSpan}(k, \\mathbb{R}^n) = \\top$$$

Lean4

/-- The span of `univ` is `⊤`. -/
@[simp]
theorem span_univ : affineSpan k (Set.univ : Set P) = ⊤ :=
  eq_top_iff.2 <| subset_affineSpan k _

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

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

Разделы

Аффилиация

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