modelWithCorners_prod_coe_symm — Mathlib

English

The symmetric (inverse) product equivalence also commutes: ((I.prod J).symm) = Prod.map I.symm I'.symm.

Русский

Обратное отображение в произведении равно произведению обратных отображений.

LaTeX

$$((I.prod J).symm) = Prod.map I.symm I'.symm$$

Lean4

@[simp, mfld_simps]
theorem modelWithCorners_prod_coe_symm (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') :
    ((I.prod I').symm : _ × _ → _ × _) = Prod.map I.symm I'.symm :=
  rfl

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