English
If two adjoint relations fit in a chain B ⟶ B' and B' ⟶ B'', then composing the forward maps and the backward maps yields an adjoint relation between B and B'' with the composed forward and backward maps: f'∘f and g∘g'.
Русский
Если две пары сопряжённости образуют цепочку B ⟶ B' и B' ⟶ B'', то композиция соответствующих прямых и обратных отображений дает пару сопряжённости между B и B'' с составными отображениями f'∘f и g∘g'.
LaTeX
$$$IsAdjointPair(B,B'')(f'\\circ f,\\, g\\circ g')$, given $IsAdjointPair(B,B',f,g)$ and $IsAdjointPair(B',B'',f',g')$.$$
Lean4
theorem comp {f : M → M₁} {g : M₁ → M} {f' : M₁ → M₂} {g' : M₂ → M₁} (h : IsAdjointPair B B' f g)
(h' : IsAdjointPair B' B'' f' g') : IsAdjointPair B B'' (f' ∘ f) (g ∘ g') := fun _ _ ↦ by
rw [Function.comp_def, Function.comp_def, h', h]
