repr_range

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#LinearIndependent.repr_range

English

The range of the repr map is the entire span of the independent family, i.e., the whole space.

Русский

Область определения отображения repr равна всему покрытию независимой семьи.

LaTeX

$$$\\operatorname{range}(hv.repr) = \\top$ in the span$$

Lean4

theorem repr_range : LinearMap.range hv.repr = ⊤ := by rw [LinearIndependent.repr, LinearEquiv.range]

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

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

Разделы

Аффилиация

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