toBinaryBiconeIsBilimit — Mathlib

English

Auxiliary step in establishing the bilimit equivalence; demonstrates one direction of the correspondence between bilimit properties.

Русский

Вспомогательный шаг в доказательстве эквивалентности билилимита; демонстрирует одно направление соответствия свойств билилимита.

LaTeX

$$$ \text{IsBilimit}(b) \Rightarrow \text{IsBilimit}(b.toBinaryBicone) $$$

Lean4

/-- A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a
bilimit. -/
def toBinaryBiconeIsBilimit {X Y : C} (b : Bicone (pairFunction X Y)) : b.toBinaryBicone.IsBilimit ≃ b.IsBilimit
    where
  toFun h := ⟨b.toBinaryBiconeIsLimit h.isLimit, b.toBinaryBiconeIsColimit h.isColimit⟩
  invFun h := ⟨b.toBinaryBiconeIsLimit.symm h.isLimit, b.toBinaryBiconeIsColimit.symm h.isColimit⟩
  left_inv := fun ⟨h, h'⟩ => by dsimp only; simp
  right_inv := fun ⟨h, h'⟩ => by dsimp only; simp

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