English
There is a partially defined linear map from E to G obtained by composing a linear map g: F → G with a partially defined map f: E →ₗ.[R] F, provided f(x) lies in the domain of g for all x in dom(f). The resulting map has domain dom(f) and acts by x ↦ g(f(x)).
Русский
Существует частично заданное линейное отображение E → G, получаемое по композиции линейного отображения g: F → G с частично заданным отображением f: E →ₗ.[R] F, при условии, что для всех x в dom(f) значение f(x) принадлежит dom(g). Образование новой карты имеет область определения dom(f) и задаётся формулой x ↦ g(f(x)).
LaTeX
$$$\operatorname{dom}(\mathrm{compPMap}(g,f)) = \operatorname{dom}(f) \quad\text{and}\quad (\mathrm{compPMap}(g,f))(x) = g(f(x)) \text{ for } x \in \operatorname{dom}(f).$$$
Lean4
/-- Compose a linear map with a `LinearPMap` -/
def compPMap (g : F →ₗ[R] G) (f : E →ₗ.[R] F) : E →ₗ.[R] G
where
domain := f.domain
toFun := g.comp f.toFun
