English
If p and q are complementary subspaces of E with isomorphism h, then swapping the factors in p × q and using the complement projection yields the same as the complement projection with the swapped order, up to the symmetry of the decomposition.
Русский
Пусть p и q — комплементарные подпространства E и h — изоморфизм. Перестановка компонент в произведении p × q и последующая проекция обратно дают то же самое, что проекция для переставленного порядка разложения.
LaTeX
$$$\text{LinearEquiv.prodComm}\;R\;q\;p \;\llcorner\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! =\; (\mathrm{prodEquivOfIsCompl } p q h) \;\text{with } \text{prodEquivOfIsCompl } q p h^{-1}$$$
Lean4
@[simp]
theorem prodComm_trans_prodEquivOfIsCompl (h : IsCompl p q) :
LinearEquiv.prodComm R q p ≪≫ₗ prodEquivOfIsCompl p q h = prodEquivOfIsCompl q p h.symm :=
LinearEquiv.ext fun _ => add_comm _ _
