map_fst — Mathlib

English

As above, with W, X, Y, Z and f: W → Y, g: X → Z, the relation (prod.map f g) ∘ prod.fst = prod.fst ∘ f holds.

Русский

Точно так же, как и выше, выполняется (prod.map f g) ∘ prod.fst = prod.fst ∘ f.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem map_fst {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
    prod.map f g ≫ prod.fst = prod.fst ≫ f :=
  limMap_π _ _

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