binaryProductIso_inv_comp_fst — Mathlib

English

The inverse of the product isomorphism composed with the first projection equals the standard first projection.

Русский

Обратный изоморфизм бинарного произведения, композиция с проекцией fst, равна стандартной проекции fst.

LaTeX

$$$$ (binaryProductIso X Y)^{-1} \\circ Prod.fst = Prod.fst $$$$

Lean4

@[elementwise (attr := simp)]
theorem binaryProductIso_inv_comp_fst (X Y : Type u) : (binaryProductIso X Y).inv ≫ Limits.prod.fst = _root_.Prod.fst :=
  limit.isoLimitCone_inv_π (binaryProductLimitCone X Y) ⟨WalkingPair.left⟩

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