English
There is an additive action of the group of linear maps L(E,F) on the set of partial linear maps E →ₗ.[R] F, given by vadd: (f,g) ↦ f +ᵥ g, with the neutral element acting as identity and addition compatible with addition of linear maps.
Русский
Существует действие дополнения множества частичных линейных отображений со стороны группы линейных отображений L(E,F): f +ᵥ g обозначает частичное сложение, нейтральный элемент действует как тождественный, и совместимость сохраняется в сложении линейных отображений.
LaTeX
$$$$ \\exists \\,+_{\\mathrm{v}}: (L(E,F) \\times \\mathrm{LinearPMap}(R,E,F)) \\to \\mathrm{LinearPMap}(R,E,F) \\,\\Big(0_{\\mathrm{v}}: \\mathrm{LinearPMap}(R,E,F) \\to \\mathrm{LinearPMap}(R,E,F)\\Big) $$\nwith\n$$ f +_{\\mathrm{v}} g = f +_{\\mathrm{v}} g,\\quad 0 +_{\\mathrm{v}} g = g,\\quad f_1 +_{\\mathrm{v}} (f_2 +_{\\mathrm{v}} g) = (f_1 + f_2) +_{\\mathrm{v}} g. $$$$
Lean4
@[simp]
theorem vadd_domain (f : E →ₗ[R] F) (g : E →ₗ.[R] F) : (f +ᵥ g).domain = g.domain :=
rfl
