piIsoPi_inv_π_apply — Mathlib

English

For α, i and a family x = (x_i) with x_i ∈ α_i, applying the inverse of piIsoPi α to x and then projecting to i-th component recovers x_i.

Русский

Пусть α и индекс i заданы; для элемента x = (x_i) во всех компонентах, применение обратного к piIsoPi α к x и последующая проекция на i-ю компоненту восстанавливают x_i.

LaTeX

$$$\\Pi\\pi_{\\alpha,i}\\bigl((\\mathrm{piIsoPi}\\alpha)^{-1}x\\bigr)=x_i$$$

Lean4

theorem piIsoPi_inv_π_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : ∀ i, α i) :
    (Pi.π α i :) ((piIsoPi α).inv x) = x i :=
  ConcreteCategory.congr_hom (piIsoPi_inv_π α i) x

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