of_isBilimit — Mathlib

English

If a Bilimit structure exists for a binary bicone on X and Y, then the square with zeros forms a pullback.

Русский

Если существует bilimit-структура для двоичной биони под X и Y, то квадрат с нулями образует пуллбак.

LaTeX

$$$IsBilimit b \\Rightarrow IsPullback b.fst b.snd (0 : X \\to 0) (0 : Y \\to 0)$$$

Lean4

theorem of_isBilimit {b : BinaryBicone X Y} (h : b.IsBilimit) : IsPullback b.fst b.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) := by
  convert IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal <;> subsingleton

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