of_isPullback_isPushout — Mathlib

English

If p1 is a pullback square and p2 is a pushout square for the same c, then the square is bicartesian: BicartesianSq f g h i.

Русский

Если один квадрат является pullback, а другой — pushout для одного и того же образа, то квадрат является бикартезианским: BicartesianSq f g h i.

LaTeX

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

Lean4

theorem of_isPullback_isPushout (p₁ : IsPullback f g h i) (p₂ : IsPushout f g h i) : BicartesianSq f g h i :=
  BicartesianSq.mk p₁ p₂.isColimit'

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