productEquiv_apply — Mathlib

English

The i-th component of productEquiv applied to x equals the i-th projection of x.

Русский

i-й компонент отображения productEquiv примененного к x равен i-й проекции x.

LaTeX

$$$(\\mathrm{productEquiv}\\, X\\, x)\\!\\left(i\\right) = \\Pi\\!\\pi X\\!\\, i\\, x$$$

Lean4

@[simp]
theorem productEquiv_apply {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u}) (x : (∏ᶜ X : FintypeCat)) (i : ι) :
    productEquiv X x i = Pi.π X i x := by
  simpa [productEquiv] using (elementwise_of% piComparison_comp_π FintypeCat.incl X i) x

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