constr_basis — Mathlib

English

Applying the constr map to the basis vectors yields the prescribed f: (constr b S f)(b i) = f i.

Русский

Применение конструирования к базисным векторам даёт заданный f: (constr b S f)(b i) = f(i).

LaTeX

$$$(\\mathrm{constr}\\, b\\ S\\ f)(b i) = f(i).$$$

Lean4

@[simp]
theorem constr_basis (f : ι → M') (i : ι) : (constr (M' := M') b S f : M → M') (b i) = f i := by
  simp [Basis.constr_apply, b.repr_self]

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