of_is_biproduct₁ — Mathlib

English

If a binary bicone X ⊞ Y is bilimit, then the square with fst = biprod.fst, snd = biprod.snd and zeros is bicartesian: BicartesianSq fst snd 0 0.

Русский

Если бинарный би-диаграмма X ⊞ Y имеет свойство двукратной предельности, то соответствующий квадрат с fst = biprod.fst, snd = biprod.snd, 0 на обеих сторонах является бикартезианским: BicartesianSq fst snd 0 0.

LaTeX

$$$ \\operatorname{BicartesianSq}(\\text{biprod.fst}, \\text{biprod.snd}, 0, 0) $$$

Lean4

/-- ```
 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0
```
is a bi-Cartesian square.
-/
theorem of_is_biproduct₁ {b : BinaryBicone X Y} (h : b.IsBilimit) : BicartesianSq b.fst b.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) :=
  of_isPullback_isPushout (IsPullback.of_isBilimit h) (IsPushout.of_is_bilimit' h)

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