piCongrRight_symm — Mathlib

English

The symmetric version of piCongrRight is obtained by swapping the two index families.

Русский

Симметричная версия piCongrRight получается заменой двух семейств индексов.

LaTeX

$$$ (\pi\!CongrRight\ F)^{\mathrm{symm}} = \piCongrRight \ ((F_i)^{\mathrm{symm}}).$$$

Lean4

@[simp]
theorem piCongrRight_symm {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)] [∀ i, TopologicalSpace (Y₂ i)]
    (F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (piCongrRight F).symm = piCongrRight fun i => (F i).symm :=
  rfl

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