sub — Mathlib

English

If two endomorphisms f,g and f',g' form adjoint pairs with respect to B and B', then the pair (f−f', g−g') also forms an adjoint pair with the same pair of bilinear maps.

Русский

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

LaTeX

$$IsAdjointPair B B'(f−f',\, g−g').$$

Lean4

theorem sub (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') : IsAdjointPair B B' (f - f') (g - g') :=
  fun x _ ↦ by rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']

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