sigmaIsoSigma_hom_ι_apply — Mathlib

English

The inverse of the sigma-sigma isomorphism applied to a pair ⟨i,x⟩ equals the i-th injection of x.

Русский

Обратная к изоморфизму сигма-сигма применяется к паре ⟨i,x⟩ даёт i–ю инъекцию x.

LaTeX

$$$(\\sigma\\mathrm{iso}\\sigma α)^{-1}\\langle i,x\\rangle = (\\Sigma.ι α i)\\; x$$$

Lean4

theorem sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : α i) :
    (sigmaIsoSigma α).hom ((Sigma.ι α i :) x) = Sigma.mk i x :=
  ConcreteCategory.congr_hom (sigmaIsoSigma_hom_ι α i) x

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