prodComparison_comp — Mathlib

English

The composition of prodComparison along F and G equals the sequential coproducts: prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B).

Русский

Композиция prodComparison по F и G равна последовательному копродукту: prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B).

LaTeX

$$$ \\operatorname{prodComparison} (F \\cdot G) A B = G.map (\\operatorname{prodComparison} F A B) \\circ \\operatorname{prodComparison} G (F.obj A) (F.obj B) $$$

Lean4

theorem prodComparison_comp :
    prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B) :=
  by
  unfold prodComparison
  ext <;> simp [← G.map_comp]

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