piCongrLeft'_symm_apply — Mathlib

English

The symmetry (inverse) of piCongrLeft' corresponds to the inverse Equiv piCongrLeft'.

Русский

Обратное отображение piCongrLeft' соответствует обратному эквивалентному отображению Equiv.piCongrLeft'.

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₁ (e.symm i)) :
    (piCongrLeft' R A₁ e).symm x = (Equiv.piCongrLeft' _ _).symm x :=
  rfl

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