instAdd — Mathlib

English

There is a addition operation on LinearPMap defined by taking the intersection of domains and summing the restrictions.

Русский

Существует операция сложения на LinearPMap, определяемая пересечением доменов и суммированием ограничений.

LaTeX

$$$f + g$ имеет домен $\mathrm{dom}(f) \cap \mathrm{dom}(g)$ и $(f+g) x = f x + g x$ для $x$ в этой области.$$

Lean4

instance instAdd : Add (E →ₗ.[R] F) :=
  ⟨fun f g =>
    { domain := f.domain ⊓ g.domain
      toFun :=
        f.toFun.comp (inclusion (inf_le_left : f.domain ⊓ g.domain ≤ _)) +
          g.toFun.comp (inclusion (inf_le_right : f.domain ⊓ g.domain ≤ _)) }⟩

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