binaryCoproductIso_inl_comp_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[elementwise (attr := simp)]
theorem binaryCoproductIso_inl_comp_inv (X Y : Type u) :
    ↾(Sum.inl : X ⟶ X ⊕ Y) ≫ (binaryCoproductIso X Y).inv = Limits.coprod.inl :=
  colimit.isoColimitCocone_ι_inv (binaryCoproductColimitCocone X Y) ⟨WalkingPair.left⟩

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