toBiconeIsBilimit — Mathlib

English

Reiteration: with HasBinaryBiproduct P Q we obtain HasLimit (pair P Q).

Русский

Повторение: при наличии HasBinaryBiproduct P Q следует HasLimit (pair P Q).

LaTeX

$$$ HasBinaryBiproduct P Q \Rightarrow HasLimit(\text{pair } P Q). $$$

Lean4

/-- A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit. -/
def toBiconeIsBilimit {X Y : C} (b : BinaryBicone X Y) : b.toBicone.IsBilimit ≃ b.IsBilimit
    where
  toFun h := ⟨b.toBiconeIsLimit h.isLimit, b.toBiconeIsColimit h.isColimit⟩
  invFun h := ⟨b.toBiconeIsLimit.symm h.isLimit, b.toBiconeIsColimit.symm h.isColimit⟩
  left_inv := fun ⟨h, h'⟩ => by dsimp only; simp
  right_inv := fun ⟨h, h'⟩ => by dsimp only; simp

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