prodCongr_symm — Mathlib

English

For h1: X ≃ₜ X' and h2: Y ≃ₜ Y', we have (h1.prodCongr h2).symm = h1.symm.prodCongr h2.symm.

Русский

Для гомеоморфизмов h1 и h2 выполняется (h1.prodCongr h2).symm = h1.symm.prodCongr h2.symm.

LaTeX

$$$(h_1 : X \simeq_t X') \land (h_2 : Y \simeq_t Y') \Rightarrow (h_1.prodCongr h_2).symm = h_1.symm.prodCongr h_2.symm$$$

Lean4

@[simp]
theorem prodCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm :=
  rfl

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