isRightKanExtension — Mathlib

English

For a StrictSegal simplicial set X, there is a right Kan extension structure along the inclusion in dimension 2 making X extend canonically along that inclusion.

Русский

Для строгосегалевой симпликальной множества X существует структура правого Кан-расширения вдоль включения в размер 2, делающая X канонически продолжимым вдоль этого включения.

LaTeX

$$$ \mathrm{Ran}_{\iota_2} X \;\text{exists as a right Kan extension along the inclusion.} $$$

Lean4

theorem isRightKanExtension (sx : StrictSegal X) : X.IsRightKanExtension (𝟙 ((inclusion 2).op ⋙ X)) :=
  RightExtension.IsPointwiseRightKanExtension.isRightKanExtension sx.isPointwiseRightKanExtension

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