of_is_biproduct₂ — Mathlib

English

If p1 is IsPullback f g h i and p2 is IsPushout f g h i, then the square is bicartesian: BicartesianSq f g h i.

Русский

Если p1 — IsPullback, а p2 — IsPushout для одного и того же quadruple, то квадрат является бикартезианским: BicartesianSq f g h i.

LaTeX

$$$ \\operatorname{BicartesianSq}(f,g,h,i) $$$

Lean4

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

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