biprodComparison_snd — Mathlib

English

Under the same hypotheses as above, the second projection is compatible with F in the same manner: F.map biprod.snd = biprodComparison F X Y ≫ biprod.snd.

Русский

При тех же предпосылках вторую проекцию совместимы с отображением F аналогично: F.map biprod.snd = biprodComparison F X Y ≫ biprod.snd.

LaTeX

$$$F(\\text{biprod.snd}) = \\text{biprodComparison}(F,X,Y) \\circ \\text{biprod.snd}$$$

Lean4

@[reassoc (attr := simp)]
theorem biprodComparison_snd : biprodComparison F X Y ≫ biprod.snd = F.map biprod.snd :=
  biprod.lift_snd _ _

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