toBinaryBiconeIsLimit — Mathlib

English

A binary bicone is a bilimit if and only if the corresponding bicone is a bilimit. This reduces bilimits for the binary data to bilimits for the underlying bicone.

Русский

Бинарный бикон является билилимитом тогда и только тогда, когда соответствующий бикон является билилимитом. Таким образом билилимит бинарных данных сводится к билилимиту базового бикона.

LaTeX

$$$ b.toBinaryBicone.IsBilimit \simeq b.IsBilimit. $$$

Lean4

/-- A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit
cone. -/
def toBinaryBiconeIsLimit {X Y : C} (b : Bicone (pairFunction X Y)) :
    IsLimit b.toBinaryBicone.toCone ≃ IsLimit b.toCone :=
  IsLimit.equivIsoLimit <| Cones.ext (Iso.refl _) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp

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