English
There is a composition of two LinearPMaps that yields a new LinearPMap from E to G on the product of domains, defined by combining f and g via a restriction of f to its domain and a composition with g.
Русский
Существует композиция двух частично заданных линейных отображений, приводящая к новому LinearPMap E → G на произведении доменов, заданная объединением f и g через ограничение f до его домена и последующую композицию с g.
LaTeX
$$$\text{comp}(g,f,H) = g.toFun\circ_PMap f^{\text{codRestrict}}(\cdot) \,;\ dom(\text{comp}(g,f,H)) = \operatorname{dom}(f).$$$
Lean4
/-- Compose two `LinearPMap`s -/
def comp (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : ∀ x : f.domain, f x ∈ g.domain) : E →ₗ.[R] G :=
g.toFun.compPMap <| f.codRestrict _ H
