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