add — Mathlib

English

The set of continuous linear maps from M1 to M2 is closed under addition, defined pointwise: for f,g ∈ End_R(M1,M2) and x ∈ M1, (f+g)(x) = f(x) + g(x).

Русский

Множество непрерывных линейных отображений M1 → M2 замкнуто относительно сложения, и сумма определяется по точкам: (f+g)(x) = f(x) + g(x).

LaTeX

$$$f,g \\in \\operatorname{End}_R(M_1,M_2) \\implies f+g \\in \\operatorname{End}_R(M_1,M_2) \\text{ and } (f+g)(x) = f(x) + g(x).$$$

Lean4

instance add : Add (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun f g => ⟨f + g, f.2.add g.2⟩⟩

Похожие утверждения