prodIsoPullback_inv_fst — Mathlib

English

The inverse of the pullback-to-product is composed with prod.fst to yield the pullback.fst.

Русский

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

LaTeX

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

Lean4

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

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