coe_equivProdOfSurjectiveOfIsCompl

English

The canonical coe form of the product equivalence equals the standard product equivalence when IsCompl holds.

Русский

Каноническая форма произведения совпадает с обычной, когда IsCompl выполняется.

LaTeX

$$$$(f.equivProdOfSurjectiveOfIsCompl g) = (f.prod g).$$$$

Lean4

@[simp]
theorem coe_equivProdOfSurjectiveOfIsCompl {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 : E →ₗ[𝕜] F × G) = f.prod g :=
  rfl

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