piCongrLeft_symm_apply — Mathlib

English

The symmetry version of piCongrLeft gives (piCongrLeft R A₁ e).symm x = (Equiv.piCongrLeft A₁ e).symm x.

Русский

Обратное отображение piCongrLeft даёт (piCongrLeft R A₁ e).symm x = (Equiv.piCongrLeft A₁ e).symm x.

LaTeX

$$$$ (\pi\mathrm{CongrLeft} R A_1 e)^{-1} x = (\mathrm{Equiv}.\mathrm{piCongrLeft} A_1 e)^{-1} x. $$$$

Lean4

@[simp low]
theorem piCongrLeft_symm_apply {ι' : Type*} (e : ι' ≃ ι) (x : Π i, A₁ i) :
    (piCongrLeft R A₁ e).symm x = (Equiv.piCongrLeft _ _).symm x :=
  rfl

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