sigmaIsoSigma_inv_apply — Mathlib

English

The inverse of the sigma-sigma isomorphism sends ⟨i,x⟩ to the i-th coordinate inside the sigma object.

Русский

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

LaTeX

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

Lean4

theorem sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : α i) :
    (sigmaIsoSigma α).inv ⟨i, x⟩ = (Sigma.ι α i :) x := by
  rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id, Category.comp_id]

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