isoClosure_strictLimitsOfShape — Mathlib

English

The iso-closure of limits coincides with the limits itself: P.isoClosure.limitsOfShape J = P.limitsOfShape J.

Русский

Замыкание по изоморфизмам пределов совпадает с самими пределами: P.isoClosure.limitsOfShape J = P.limitsOfShape J.

LaTeX

$$$P^{\text{isoClosure}}.limitsOfShape(J) = P.limitsOfShape(J)$$$

Lean4

@[simp]
theorem isoClosure_strictLimitsOfShape : (P.strictLimitsOfShape J).isoClosure = P.limitsOfShape J :=
  by
  refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictLimitsOfShape_le_limitsOfShape
  · intro X ⟨h⟩
    have := h.hasLimit
    exact
      ⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
        ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩

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