piIsoPi_inv_π — Mathlib

English

For a family α: ι → TopCat, the inverse of the canonical product isomorphism piIsoPi α satisfies a coordinatewise projection relation with the i-th factor.

Русский

Для семейства α: ι → TopCat обратная сторона канонического произведения изоморфизма piIsoPi α удовлетворяет координатному отношению с i-й составляющей.

LaTeX

$$$(\\pi\\mathrm{Iso}\\,\\alpha)^{-1} \\circ \\Pi\\pi_{\\alpha,i} = \\pi_{\\alpha,i}$$$

Lean4

@[reassoc (attr := simp)]
theorem piIsoPi_inv_π {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) : (piIsoPi α).inv ≫ Pi.π α i = piπ α i := by
  simp [piIsoPi]

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