piCongrLeft'_apply — Mathlib

English

The map piCongrLeft' R A₁ e acts on x by the underlying Equiv.piCongrLeft' map; i.e., piCongrLeft' R A₁ e x = Equiv.piCongrLeft' _ _ x.

Русский

Применение piCongrLeft' действует на x так же, как и соответствующее отображение Equiv.piCongrLeft'; то есть piCongrLeft' R A₁ e x = Equiv.piCongrLeft' _ _ x.

LaTeX

$$$$ \pi\mathrm{CongrLeft}'(R, A_1, e)\;x = \mathrm{Equiv}.\mathrm{piCongrLeft}'_{A_1}(e, x). $$$$

Lean4

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

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