proj — Mathlib

English

The projection from S to the n-th component of S.diagram is given by the nth projection of the asLimitCone.

Русский

Проекция из S на n-й компонент диаграммы S задаётся как n-я проекция конуса asLimitCone.

LaTeX

$$$\\mathrm{proj}(n) : S \\to S.diagram.obj(\\langle n \\rangle) \\,=\, S.asLimitCone.\\pi.{\\langle n \\rangle}$$$

Lean4

/-- The projection from `S` to the `n`th component of `S.diagram`. -/
abbrev proj (n : ℕ) : S ⟶ S.diagram.obj ⟨n⟩ :=
  S.asLimitCone.π.app ⟨n⟩

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