diag_map_fst_snd — Mathlib

English

The diagonal on X × Y composed with prod.map fst snd is the identity on X × Y: diag(X × Y) ≫ prod.map fst snd = id_{X×Y}.

Русский

Диагональ на X × Y, соединённая с prod.map fst snd, даёт тождество на X × Y: diag(X × Y) ≫ prod.map fst snd = id_{X×Y}.

LaTeX

$$$diag(X \\times Y) \\\\circ prod.map fst snd = id_{X \\times Y}$$$

Lean4

@[reassoc]
theorem diag_map_fst_snd {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] :
    diag (X ⨯ Y) ≫ prod.map prod.fst prod.snd = 𝟙 (X ⨯ Y) := by simp

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