productEquiv_symm_apply_π — Mathlib

English

For x in ToType(∏ᶜ F) and j ∈ J, productEquiv F x j equals the j-th projection of x along F j.

Русский

Для x из ToType(∏ᶜ F) и j ∈ J, productEquiv F x j равен j-ой проекции x через F j.

LaTeX

$$$ \\mathrm{productEquiv} F \\; x \\; j = \\Pi^\\mathsf{π} F j \\; x $$$

Lean4

@[simp]
theorem productEquiv_symm_apply_π (x : ∀ j, ToType (F j)) (j : J) : Pi.π F j ((productEquiv F).symm x) = x j := by
  rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]

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