constr_self

Mathlib.LinearAlgebra.Basis.Defs

URI: https://scilib.ai/kg/mathlib#Module.Basis.constr_self

English

The range of constr is the span of the set {f(i) : i ∈ ι}.

Русский

Образ отображения constr есть оболочка множества {f(i) : i ∈ ι}.

LaTeX

$$$\\mathrm{range}(\\mathrm{constr}\\ b\\ S\\ f) = \\mathrm{span}_R(\\mathrm{range}(f)).$$$

Lean4

theorem constr_self (f : M →ₗ[R] M') : (constr (M' := M') b S fun i => f (b i)) = f :=
  b.constr_eq S fun _ => rfl

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

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

Разделы

Аффилиация

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