prod_symm — Mathlib

English

The product of identity maps on X and Y equals the identity on X×Y.

Русский

Произведение тождественных отображений на X и Y равно тождественному на X×Y.

LaTeX

$$$ (\OpenPartialHomeomorph.refl X).prod (\OpenPartialHomeomorph.refl Y) = \OpenPartialHomeomorph.refl (X \times Y) $$$

Lean4

@[simp, mfld_simps]
theorem prod_symm (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') :
    (eX.prod eY).symm = eX.symm.prod eY.symm :=
  rfl

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