w_prod_fst — Mathlib

English

Let X, Y be objects in StructuredArrow (S,S')(T × T') and f: X → Y. Then the first projection of X composed with T.map f.right.1 equals the first projection of Y: X.hom.fst ≫ T.map f.right.fst = Y.hom.fst.

Русский

Пусть X, Y — объекты в StructuredArrow (S,S')(T × T'), и f: X → Y. Тогда X.hom.fst ∘ T.map f.right.fst = Y.hom.fst.

LaTeX

$$$X,hom,fst \;:\; X.hom.fst ≫ T.map f.right.fst = Y.hom.fst$$$

Lean4

@[reassoc (attr := simp)]
theorem w_prod_fst {X Y : StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y) : X.hom.1 ≫ T.map f.right.1 = Y.hom.1 :=
  congr_arg _root_.Prod.fst (StructuredArrow.w f)

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