piCongrLeft — Mathlib

English

This is the reindexing of dependent functions expressed as an AlgEquiv, obtained from piCongrLeft' by inverting the indexing Equiv.

Русский

Это переиндексация зависимых функций, выраженная как алгебраическое эквивалентное отображение, полученное из piCongrLeft' через инверсию эквививента индексов.

LaTeX

$$$$ \Pi_i A_1 i \simeq_R \Pi_i A_1 (e.symm i) $$$$

Lean4

/-- Transport dependent functions through an equivalence of the base space, expressed as
"simplification".

This is `Equiv.piCongrLeft` as an `AlgEquiv`.
-/
def piCongrLeft {ι' : Type*} (e : ι' ≃ ι) : (Π i, A₁ (e i)) ≃ₐ[R] Π i, A₁ i :=
  (AlgEquiv.piCongrLeft' R A₁ e.symm).symm

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