add — Mathlib

English

If (f,g) and (f',g') are adjoint pairs, then (f+f', g+g') is also an adjoint pair.

Русский

Если пары (f,g) и (f',g') взаимно сопряжены, то и сумма образует сопряжённую пару.

LaTeX

$$If h: IsAdjointPair B B' f g and h': IsAdjointPair B B' f' g', then IsAdjointPair B B' (f+f') (g+g').$$

Lean4

theorem add {f f' : M → M₁} {g g' : M₁ → M} (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') :
    IsAdjointPair B B' (f + f') (g + g') := fun x _ ↦ by
  rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, h, h']

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