English
The construction Function.ExtendByZero.hom R s provides a linear map from (ι → R) to (η → R) by extending f by zero outside s.
Русский
Конструкция Function.ExtendByZero.hom R s задаёт линейное отображение из (ι → R) в (η → R) путём продолжения f нулём вне области s.
LaTeX
$$$$ \\text{linearMap} : (ι \\to R) \\to_{R} (η \\to R) \n\\text{defined by } (\\text{linearMap } f)(t)=\\text{extend } s f 0 (t). $$$$
Lean4
/-- `Function.extend s f 0` as a bundled linear map. -/
@[simps]
noncomputable def linearMap : (ι → R) →ₗ[R] η → R :=
{ Function.ExtendByZero.hom R s with
toFun := fun f => Function.extend s f 0
map_smul' := fun r f => by simpa using Function.extend_smul r s f 0 }
