English
Define the partially defined map f.coprod g on E × F to G by domain dom(f) × dom(g) and value (e,f) ↦ f(e) + g(f).
Русский
Определим частично заданное отображение f.coprod g: dom(f) × dom(g) → G, задаваемое как (e,f) ↦ f(e) + g(f).
LaTeX
$$$\operatorname{dom}(f\mathrm{ coprod } g) = \operatorname{dom}(f) \times \operatorname{dom}(g),\quad (f\mathrm{ coprod } g)((e,f)) = f(e) + g(f).$$$
Lean4
/-- `f.coprod g` is the partially defined linear map defined on `f.domain × g.domain`,
and sending `p` to `f p.1 + g p.2`. -/
def coprod (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) : E × F →ₗ.[R] G
where
domain := f.domain.prod g.domain
toFun :=
(show f.domain.prod g.domain →ₗ[R] G from (f.comp (LinearPMap.fst f.domain g.domain) fun x => x.2.1).toFun) +
(show f.domain.prod g.domain →ₗ[R] G from (g.comp (LinearPMap.snd f.domain g.domain) fun x => x.2.2).toFun)
