comp_diag — Mathlib

English

Let W × X and Y × Z be binary products. For f: W → Y and g: X → Z, the map prod.map f g composed with prod.fst equals prod.fst composed with f, i.e., (prod.map f g) ∘ fst = fst ∘ f.

Русский

Пусть W × X и Y × Z — бинарные произведения. Для f: W → Y и g: X → Z выполняется (prod.map f g) ∘ fst = fst ∘ f.

LaTeX

$$$prod.map \\, f \\, g \\circ fst = fst \\circ f$$$

Lean4

theorem comp_diag {X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) : f ≫ diag Y = prod.lift f f := by simp

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