of_has_biproduct₁ — Mathlib

English

If b is a BinaryBicone X Y with IsBilimit, then both squares with inl/inr to 0 are bicartesian: BicartesianSq 0 0 inl inr.

Русский

Если b — бинарный би-косин, имеющий IsBilimit, то квадраты 0 ⟶ X, 0 ⟶ Y, with inl/inr to X ⊕ Y образуют бикартезианский квадрат: BicartesianSq 0 0 inl inr.

LaTeX

$$$ \\operatorname{BicartesianSq}(0,0,\\text{inl},\\text{inr}) $$$

Lean4

/-- ```
 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0
```
is a bi-Cartesian square.
-/
@[simp]
theorem of_has_biproduct₁ [HasBinaryBiproduct X Y] : BicartesianSq biprod.fst biprod.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) := by
  convert of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)

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