lapply — Mathlib

English

The map that takes a family of linear maps (lapply i) is injective into the product of maps.

Русский

Отображение, взятое попарно для всех i, инъективно; смысл: если их координатные планы совпадают, то сами отображения совпадают.

LaTeX

$$$\\text{injective }(\\mathrm{LinearMap.pi}\\, (R := R)\\, \\lvert\\, \\mathrm{lapply})$$$

Lean4

/-- Interpret `fun (f : Π₀ i, M i) ↦ f i` as a linear map. -/
def lapply (i : ι) : (Π₀ i, M i) →ₗ[R] M i where
  toFun f := f i
  map_add' f g := add_apply f g i
  map_smul' c f := smul_apply c f i

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