productIso_inv_comp_π — Mathlib

English

For a small J and F: J → Type, and j ∈ J, (productIso F)^{-1} ∘ Pi.π F j = ((equivShrink (∀ j, F j)).symm) .? j

Русский

Для маленького множества J и F: J → Type, и j ∈ J, (productIso F)^{-1} ∘ Pi.π F j = ((equivShrink (∀ j, F j)).symm) j.

LaTeX

$$$$ (productIso.{v,u} F)^{-1} \\circ \\Pi\\!\\pi F j = ((equivShrink (\\forall j, F j)).symm) j $$$$

Lean4

@[elementwise (attr := simp)]
theorem productIso_inv_comp_π (j : J) :
    (productIso.{v, u} F).inv ≫ Pi.π F j = fun f => ((equivShrink (∀ j, F j)).symm f) j :=
  limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩

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