subspaceInhabited

Mathlib.LinearAlgebra.Projectivization.Subspace

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

English

The span of a subspace is the subspace (simp lemma).

Русский

Лемма упрощения: span подпространства возвращает то же подпространство.

LaTeX

$$$\operatorname{span}(\uparrow W) = W$$$

Lean4

instance subspaceInhabited : Inhabited (Subspace K V) where default := ⊤

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

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

Разделы

Аффилиация

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