desc_inl_inr — Mathlib

English

The canonical coprod.desc of the injections is the identity on the coproduct X ⨿ Y: coprod.desc coprod.inl coprod.inr = id_(X ⨿ Y).

Русский

Универсальный стрелок coprod.desc по инъекциям inl и inr равен тождественному на копродукте X ⨿ Y.

LaTeX

$$$ coprod.desc coprod.inl coprod.inr = id_{X \sqcup Y}.$$$

Lean4

@[simp]
theorem desc_inl_inr {X Y : C} [HasBinaryCoproduct X Y] : coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y) := by
  ext <;>
    simp
      -- The simp linter says simp can prove the reassoc version of this lemma.

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