English
Let f: E → F be a linear map and g ∈ E →ₗ.[R] F a partial linear map with domain dom(g). Define the sum f +ᵥ g to be the partial linear map with domain dom(g) and value (f +ᵥ g)(x) = f(x) + g(x) for x ∈ dom(g). This endows the pair with a natural vector-like addition.
Русский
Пусть f: E → F — линейное отображение, а g — частичное линейное отображение с областью dom(g). Определим сумму f +ᵥ g как частичное линейное отображение с доменом dom(g) и значением (f +ᵥ g)(x) = f(x) + g(x) при x ∈ dom(g).
LaTeX
$$$$ (f+_{\\mathrm{v}} g)\\text{ имеет } \\operatorname{dom}(f+_{\\mathrm{v}} g)=\\operatorname{dom}(g),\\quad (f+_{\\mathrm{v}} g)(x)=f(x)+g(x)\\text{ для } x\\in\\operatorname{dom}(g). $$$$
Lean4
instance instVAdd : VAdd (E →ₗ[R] F) (E →ₗ.[R] F) :=
⟨fun f g =>
{ domain := g.domain
toFun := f.comp g.domain.subtype + g.toFun }⟩
