prodCongr_symm — Mathlib

English

Reiterates that swapping coordinates gives an equivalence between products.

Русский

Повторение того, что перестановка координат задаёт эквивалентность между произведениями.

LaTeX

$$$\\text{prodComm }(\\alpha,\\beta):\\alpha\\times\\beta\\simeq\\beta\\times\\alpha$$$

Lean4

@[simp, grind =]
theorem prodCongr_symm {α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
    (prodCongr e₁ e₂).symm = prodCongr e₁.symm e₂.symm :=
  rfl

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