instIsSplitEpiBiprodComparison — Mathlib

English

The map biprodComparison F X Y is an epimorphism and, in fact, split epi, under the stated hypotheses.

Русский

Отображение biprodComparison F X Y является эпиморфизмом и, фактически, явным разложимым эпиморфизмом при заданных предпосылках.

LaTeX

$$$\\text{IsSplitEpi}(\\text{biprodComparison}(F,X,Y))$$$

Lean4

instance : IsSplitEpi (biprodComparison F X Y) :=
  IsSplitEpi.mk' (splitEpiBiprodComparison F X Y)

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