prodIsoProd_hom_snd — Mathlib

English

Similarly, (prodIsoProd X Y).hom ∘ prodSnd = Limits.prod.snd.

Русский

Аналогично, (prodIsoProd X Y).hom ∘ prodSnd = Limits.prod.snd.

LaTeX

$$$(\\mathrm{prodIsoProd}(X,Y)).hom \\circ \\mathrm{prodSnd} = \\mathrm{Limits.prod.snd}$$$

Lean4

@[reassoc (attr := simp)]
theorem prodIsoProd_hom_snd (X Y : TopCat.{u}) : (prodIsoProd X Y).hom ≫ prodSnd = Limits.prod.snd :=
  by
  simp [← Iso.eq_inv_comp, prodIsoProd]
  rfl
    -- Note that `(x : X ⨯ Y)` would mean `(x : ↑X × ↑Y)` below:

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