π_mk — Mathlib

English

If x is a compatible family in the limit, then the j-th projection of the constructed limit from x equals x_j.

Русский

Если x — совместимая семья в пределе, то у j-й проекции лимита, построенного из x, равняется x_j.

LaTeX

$$$\pi_F j (\mathrm{Limit.mk} F x h) = x_j.$$$

Lean4

@[simp]
theorem π_mk (x : ∀ j, F.obj j) (h : ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j') (j) :
    limit.π F j (Limit.mk F x h) = x j := by
  dsimp [Limit.mk]
  simp
    -- PROJECT: prove this for concrete categories where the forgetful functor preserves limits

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