coe_equivProdOfSurjectiveOfIsCompl

English

The coe of the equivalence to the product map equals the product map itself.

Русский

Сопоставление канонической эквивалентности с отображением в произведение совпадает с отображением в произведение.

LaTeX

$$$(equivProdOfSurjectiveOfIsCompl f g hf hg hfg) : E\to F \times G = f.prod g$$$

Lean4

@[simp]
theorem coe_equivProdOfSurjectiveOfIsCompl {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤) (hg : range g = ⊤)
    (hfg : IsCompl (ker f) (ker g)) : (equivProdOfSurjectiveOfIsCompl f g hf hg hfg : E →ₗ[R] F × G) = f.prod g :=
  rfl

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