productEquiv_apply_apply — Mathlib

English

The same product equivalence in the concrete setting: ToType(∏ᶜ F) ≃ ∏ ToType(F j).

Русский

Та же эквивалентность произведения в конкретном контексте: ToType(∏ᶜ F) ≃ ∏ ToType(F j).

LaTeX

$$$ ToType(\\prod^\\mathsf{c} F) \\simeq \\prod_j ToType(F j) $$$

Lean4

@[simp]
theorem productEquiv_apply_apply (x : ToType (∏ᶜ F)) (j : J) : productEquiv F x j = Pi.π F j x :=
  congr_fun (piComparison_comp_π (forget C) F j) x

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