constr_eq — Mathlib

English

The constr map recovers the original map f when f is defined by evaluating on the basis: constr b S (i ↦ f(b i)) = f.

Русский

Если функция f задана через значения на базисе, то конструирование восстанавливает f: constr b S (i ↦ f(b i)) = f.

LaTeX

$$$\\mathrm{constr}\\, (M' := M')\\; b\\; S\\; (\\lambda i. f(b i)) = f.$$$

Lean4

theorem constr_eq {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ i, g i = f (b i)) : constr (M' := M') b S g = f :=
  b.ext fun i => (b.constr_basis S g i).trans (h i)

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