limitConeIsLimit — Mathlib

Lean4
/-- The chosen cone `TopCat.limitCone F` for a functor `F : J ⥤ TopCat` is a limit cone.
Generally you should just use `limit.isLimit F`, unless you need the actual definition
(which is in terms of `Types.limitConeIsLimit`).
-/
def limitConeIsLimit (F : J ⥤ TopCat.{max v u}) : IsLimit (limitCone.{v, u} F)
    where
  lift
    S :=
    ofHom
      { toFun := fun x =>
          ⟨fun _ => S.π.app _ x, fun f => by
            dsimp
            rw [← S.w f]
            rfl⟩
        continuous_toFun :=
          Continuous.subtype_mk (continuous_pi fun j => (S.π.app j).hom.2) fun x i j f =>
            by
            dsimp
            rw [← S.w f]
            rfl }
  uniq S m
    h := by
    ext a
    simp [← h]
    rfl
Похожие утверждения