prodIsoPullback_inv_snd — Mathlib

English

The inverse of the pullback-to-product composed with prod.snd gives pullback.snd.

Русский

Обратный изоморфизм pullback к произведению, затем компонуется с prod.snd, даёт pullback.snd.

LaTeX

$$$(prodIsoPullback X Y).inv \\;\\gg\\; prod.snd = pullback.snd _ _$$$

Lean4

@[reassoc (attr := simp)]
theorem prodIsoPullback_inv_snd [HasTerminal C] [HasPullbacks C] (X Y : C) [HasBinaryProduct X Y] :
    (prodIsoPullback X Y).inv ≫ prod.snd = pullback.snd _ _ :=
  limit.isoLimitCone_inv_π (limitConeOfTerminalAndPullbacks _) ⟨.right⟩

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