equivProdOfSurjectiveOfIsCompl_toLinearEquiv

English

The produced continuous linear equivalence from a product via surjective maps agrees with the standard linear product equivalence.

Русский

Полученное линейное эквивалентное отображение через произведение согласуется со стандартным линейным эквивалентом произведения.

LaTeX

$$$$ (f \equivProdOfSurjectiveOfIsCompl g)_{toLinearEquiv} = {f \equivProdOfSurjectiveOfIsCompl g hf hg hfg} $$$$

Lean4

@[simp]
theorem equivProdOfSurjectiveOfIsCompl_toLinearEquiv {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : range f = ⊤)
    (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) :
    (equivProdOfSurjectiveOfIsCompl f g hf hg hfg).toLinearEquiv =
      LinearMap.equivProdOfSurjectiveOfIsCompl f g hf hg hfg :=
  rfl

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