span_empty

Mathlib.LinearAlgebra.Projectivization.Subspace

URI: https://scilib.ai/kg/mathlib#Projectivization.Subspace.span_empty

English

The span of the empty set is the bottom of the lattice of subspaces.

Русский

Объём образ Span пустого множества равен нулю нижнего предела решётки подпространств.

LaTeX

$$$\operatorname{span}(\emptyset) = \bot$$$

Lean4

/-- The span of the empty set is the bottom of the lattice of subspaces. -/
@[simp]
theorem span_empty : span (∅ : Set (ℙ K V)) = ⊥ :=
  gi.gc.l_bot

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

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

Разделы

Аффилиация

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