productEquiv_symm_comp_π_apply — Mathlib

English

The i-th projection of the inverse image under productEquiv equals the i-th component.

Русский

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

LaTeX

$$$\\Pi X i ((\\mathrm{productEquiv} X)^{-1} x) = x_i$$$

Lean4

@[simp]
theorem productEquiv_symm_comp_π_apply {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u}) (x : ∀ i, X i) (i : ι) :
    Pi.π X i ((productEquiv X).symm x) = x i := by rw [← productEquiv_apply, Equiv.apply_symm_apply]

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