English
The block lower diagonal construction yields a continuous linear equivalence corresponding to a block matrix with diagonal blocks e and e' and a lower-off-diagonal block f.
Русский
Построение по блочным нижним диагоналям даёт непрерывно-линейное эквивалентное отображение, соответствующее блочно-матрице с диагональными блоками e, e' и нижним блоком f.
LaTeX
$$$ e:\\ M \\to M_2, \\; e' : M_3 \\to M_4, \\; f: M \\to L^R M_4 \\quad\\Rightarrow\\quad e.skewProd\, e'\, f : (M \\times M_3) \\simeq_L[R] (M_2 \\times M_4) $$$
Lean4
/-- Equivalence given by a block lower diagonal matrix. `e` and `e'` are diagonal square blocks,
and `f` is a rectangular block below the diagonal. -/
def skewProd (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) : (M × M₃) ≃L[R] M₂ × M₄ :=
{
e.toLinearEquiv.skewProd e'.toLinearEquiv
↑f with
continuous_toFun :=
(e.continuous_toFun.comp continuous_fst).prodMk
((e'.continuous_toFun.comp continuous_snd).add <| f.continuous.comp continuous_fst)
continuous_invFun :=
(e.continuous_invFun.comp continuous_fst).prodMk
(e'.continuous_invFun.comp <|
continuous_snd.sub <| f.continuous.comp <| e.continuous_invFun.comp continuous_fst) }
