productIsProduct' — Mathlib

English

The cone Pi.cone X is a limit cone for the functor X: Discrete α ⥤ C, where α is finite or general.

Русский

Конус Pi.cone X является предел-кононом для F: Discrete α ⥤ C.

LaTeX

$$IsLimit (Pi.cone X)$$

Lean4

/-- The cone `Pi.cone X` is a limit cone. -/
def productIsProduct' : IsLimit (Pi.cone X)
    where
  lift s := Pi.lift (fun j => s.π.app ⟨j⟩)
  fac s := by simp
  uniq s m
    hm := by
    dsimp
    ext
    simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
    apply hm

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