prodComparison_fst — Mathlib

English

In a functorial setting, the first projection after prodComparison corresponds to applying F to the first projection: prodComparison F A B ≫ prod.fst = F.map prod.fst.

Русский

В факторном контексте первая проекция после prodComparison равна отображению F на первую проекцию: prodComparison F A B ≫ prod.fst = F.map prod.fst.

LaTeX

$$$ \\operatorname{prodComparison} F A B \\; \\gg \\operatorname{prod.fst} = F.map \\operatorname{prod.fst}$$$

Lean4

@[reassoc (attr := simp)]
theorem prodComparison_fst : prodComparison F A B ≫ prod.fst = F.map prod.fst :=
  prod.lift_fst _ _

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