refl_prod_refl — Mathlib

English

The product of identity charts is the identity chart on the product.

Русский

Произведение тождественных карт — это тождественная карта на произведение.

LaTeX

$$$ (PartialEquiv.refl \\alpha).prod (PartialEquiv.refl \\beta) = PartialEquiv.refl (\\alpha × \\beta) $$$

Lean4

@[simp, mfld_simps]
theorem refl_prod_refl : (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β) := by
  ext ⟨x, y⟩ <;> simp

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