equivProdOfSurjectiveOfIsCompl — Mathlib

English

If f and g are surjective linear maps with IsCompl(ker f, ker g), then E is linearly isomorphic to F × G via x ↦ (f x, g x).

Русский

Если f и g сюръективны и ker f и ker g дополнения взаимно, то E изоморфно F × G по x ↦ (f x, g x).

LaTeX

$$$$E \cong F \times G.$$$$

Lean4

/-- If `f : E →L[R] F` and `g : E →L[R] G` are two surjective linear maps and
their kernels are complement of each other, then `x ↦ (f x, g x)` defines
a linear equivalence `E ≃L[R] F × G`. -/
nonrec def equivProdOfSurjectiveOfIsCompl (f : E →L[𝕜] F) (g : E →L[𝕜] G) (hf : range f = ⊤) (hg : range g = ⊤)
    (hfg : IsCompl (ker f) (ker g)) : E ≃L[𝕜] F × G :=
  (f.equivProdOfSurjectiveOfIsCompl (g : E →ₗ[𝕜] G) hf hg hfg).toContinuousLinearEquivOfContinuous
    (f.continuous.prodMk g.continuous)

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