binaryProductIso_inv_comp_fst — Mathlib

English

For functors F,G: C → Type, the first projection composed with the inverse of the binary product is equal to the first component.

Русский

Для функторов F,G: C → Type, компоновка первой проекции с обратным двоичного произведения равна первой компоненте.

LaTeX

$$$ (\mathrm{prod.fst}\ (X := F)) \circ (binaryProductIso F G)^{-1} = \mathrm{fst}$$$

Lean4

@[simp]
theorem binaryProductIso_inv_comp_fst : (binaryProductIso F G).inv ≫ Limits.prod.fst = prod.fst := by
  simp [binaryProductIso, binaryProductLimitCone]

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