instPreadditive — Mathlib

English

The category TopModuleCat is preadditive: composition is bilinear in each argument, i.e. for all f,g,h, (f ≫ g) + (f ≫ h) = f ≫ (g + h) and (f + g) ≫ h = f ≫ h + g ≫ h.

Русский

Категория TopModuleCat предадитивна: композиция билинейна по каждому аргументу, т.е. для любых f,g,h выполняются тождества (f ≫ g) + (f ≫ h) = f ≫ (g + h) и (f + g) ≫ h = f ≫ h + g ≫ h.

LaTeX

$$$ \forall f,g,h: (f \gg g) + (f \gg h) = f \gg (g + h) \quad\wedge\quad (f + g) \gg h = f \gg h + g \gg h$$$

Lean4

instance : Preadditive (TopModuleCat R)
    where
  add_comp _ _ _ _ _ _ := ConcreteCategory.ext (ContinuousLinearMap.comp_add _ _ _)
  comp_add _ _ _ _ _ _ := ConcreteCategory.ext (ContinuousLinearMap.add_comp _ _ _)

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