piCongrLeft_apply — Mathlib

English

The apply behavior of piCongrLeft' is the same as the underlying Equiv.piCongrLeft' on x.

Русский

Поведение применения piCongrLeft' совпадает с основным отображением 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₁ (e i)) :
    piCongrLeft R A₁ e x = Equiv.piCongrLeft _ _ x :=
  rfl

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